equal
deleted
inserted
replaced
100 established at the end of a proof are properly identified in the theorem |
100 established at the end of a proof are properly identified in the theorem |
101 statement. |
101 statement. |
102 |
102 |
103 * Command 'proof' provides information about proof outline with cases, |
103 * Command 'proof' provides information about proof outline with cases, |
104 e.g. for proof methods "cases", "induct", "goal_cases". |
104 e.g. for proof methods "cases", "induct", "goal_cases". |
|
105 |
|
106 * Completion templates for commands involving "begin ... end" blocks, |
|
107 e.g. 'context', 'notepad'. |
105 |
108 |
106 |
109 |
107 *** Isar *** |
110 *** Isar *** |
108 |
111 |
109 * The defining position of a literal fact \<open>prop\<close> is maintained more |
112 * The defining position of a literal fact \<open>prop\<close> is maintained more |