equal
deleted
inserted
replaced
90 "inductive_cases" |
90 "inductive_cases" |
91 "init_toplevel" |
91 "init_toplevel" |
92 "instance" |
92 "instance" |
93 "interpret" |
93 "interpret" |
94 "interpretation" |
94 "interpretation" |
|
95 "invoke" |
95 "judgment" |
96 "judgment" |
96 "kill" |
97 "kill" |
97 "kill_thy" |
98 "kill_thy" |
98 "lemma" |
99 "lemma" |
99 "lemmas" |
100 "lemmas" |
218 "defines" |
219 "defines" |
219 "domains" |
220 "domains" |
220 "elimination" |
221 "elimination" |
221 "file" |
222 "file" |
222 "fixes" |
223 "fixes" |
|
224 "for" |
|
225 "if" |
223 "imports" |
226 "imports" |
224 "in" |
227 "in" |
225 "includes" |
228 "includes" |
226 "induction" |
229 "induction" |
227 "infix" |
230 "infix" |
435 |
438 |
436 (defconst isar-keywords-proof-goal |
439 (defconst isar-keywords-proof-goal |
437 '("have" |
440 '("have" |
438 "hence" |
441 "hence" |
439 "interpret" |
442 "interpret" |
|
443 "invoke" |
440 "show" |
444 "show" |
441 "thus")) |
445 "thus")) |
442 |
446 |
443 (defconst isar-keywords-proof-block |
447 (defconst isar-keywords-proof-block |
444 '("next" |
448 '("next" |