equal
deleted
inserted
replaced
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 |