*** Prover IDE -- Isabelle/Scala/jEdit *** * Additional abbreviations for syntactic completion may be specified within the theory header as 'abbrevs', in addition to global $ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs as before. The theory syntax for 'keywords' has been simplified accordingly: optional abbrevs need to go into the new 'abbrevs' section.
This refers to Isabelle/4854f7ee0987. Examples are in src/HOL/Nonstandard_Analysis/HSEQ.thy src/HOL/Nonstandard_Analysis/HLim.thy In other words, input methods for sophisticated notation may be easily managed in a non-intrusive manner. Maybe this helps to discontinue odd ASCII art in applications. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev