In the Isabelle IDE jedit, I would like to input the following non-ascii symbol ⇩ which is used in locales/classes.
Despite many googling attempts, I could not manage to find how to do this (apart from copy-pasting the symbol). How do I input ⇩ ?
More generally, is there an easy way to find how to input a given symbol that I encounter in some Isabelle theory ?
I personally input ⇩ by typing \sub and when the autocomplete popup shows complete by pressing Tab. You can also find it and other symbols in the "Symbols" tab located by default at the bottom of jedit. ⇩ is found under the "Control" subtab there.
A list of all available symbols can be found in Appendix B of The Isabelle/Isar Reference Manual. The "input and autocomplete" method should work for all of these.