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