NEWS
changeset 63581 a1bdc546f276
parent 63579 73939a9b70a3
child 63592 64db21931bcb
equal deleted inserted replaced
63580:7f06347a5013 63581:a1bdc546f276
   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 
   113 
   114 * Additional abbreviations for syntactic completion may be specified in
   114 * Additional abbreviations for syntactic completion may be specified
   115 within the theory header as 'abbrevs', in addition to global
   115 within the theory header as 'abbrevs', in addition to global
   116 $ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs. The
   116 $ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs as
   117 theory syntax for 'keywords' has been simplified accordingly: optional
   117 before. The theory syntax for 'keywords' has been simplified
   118 abbrevs need to go into the new 'abbrevs' section.
   118 accordingly: optional abbrevs need to go into the new 'abbrevs' section.
   119 
   119 
   120 
   120 
   121 *** Isar ***
   121 *** Isar ***
   122 
   122 
   123 * 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