NEWS
changeset 63579 73939a9b70a3
parent 63560 3e3097ac37d1
child 63581 a1bdc546f276
equal deleted inserted replaced
63578:e8990d0e3965 63579:73939a9b70a3
   108 * Command 'proof' provides information about proof outline with cases,
   108 * Command 'proof' provides information about proof outline with cases,
   109 e.g. for proof methods "cases", "induct", "goal_cases".
   109 e.g. for proof methods "cases", "induct", "goal_cases".
   110 
   110 
   111 * Completion templates for commands involving "begin ... end" blocks,
   111 * Completion templates for commands involving "begin ... end" blocks,
   112 e.g. 'context', 'notepad'.
   112 e.g. 'context', 'notepad'.
       
   113 
       
   114 * Additional abbreviations for syntactic completion may be specified in
       
   115 within the theory header as 'abbrevs', in addition to global
       
   116 $ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs. The
       
   117 theory syntax for 'keywords' has been simplified accordingly: optional
       
   118 abbrevs need to go into the new 'abbrevs' section.
   113 
   119 
   114 
   120 
   115 *** Isar ***
   121 *** Isar ***
   116 
   122 
   117 * The defining position of a literal fact \<open>prop\<close> is maintained more
   123 * The defining position of a literal fact \<open>prop\<close> is maintained more