[isabelle-dev] NEWS: abbrevs within theory header
Makarius
makarius at sketis.net
Tue Aug 2 22:49:10 CEST 2016
*** 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
More information about the isabelle-dev
mailing list