isabellejedit

How can I enter symbols from set theory in Isabelle/jEdit?


How can I enter symbols like ∈, ⊆, ∪, and ∩ in Isabelle/jEdit? The Isabelle/HOL tutorial says, I should enter “:”, “<=”, “Un”, and “Int”. However, “<=” gives ≤, and the others are not translated to any symbols at all.

The only option I see so far is entering something like “\<in>” or a prefix thereof and selecting the desired symbol with the mouse. However, I want a keyboard-only input method.


Solution

  • You can type \in and then use tab to select the desired symbol, and also up/down arrow keys to select from the options.