equal
deleted
inserted
replaced
94 "inductive_cases" |
94 "inductive_cases" |
95 "init_toplevel" |
95 "init_toplevel" |
96 "instance" |
96 "instance" |
97 "interpret" |
97 "interpret" |
98 "interpretation" |
98 "interpretation" |
|
99 "invoke" |
99 "judgment" |
100 "judgment" |
100 "kill" |
101 "kill" |
101 "kill_thy" |
102 "kill_thy" |
102 "lemma" |
103 "lemma" |
103 "lemmas" |
104 "lemmas" |
228 "contains" |
229 "contains" |
229 "defines" |
230 "defines" |
230 "distinct" |
231 "distinct" |
231 "file" |
232 "file" |
232 "fixes" |
233 "fixes" |
|
234 "for" |
233 "hints" |
235 "hints" |
|
236 "if" |
234 "imports" |
237 "imports" |
235 "in" |
238 "in" |
236 "includes" |
239 "includes" |
237 "induction" |
240 "induction" |
238 "infix" |
241 "infix" |
458 |
461 |
459 (defconst isar-keywords-proof-goal |
462 (defconst isar-keywords-proof-goal |
460 '("have" |
463 '("have" |
461 "hence" |
464 "hence" |
462 "interpret" |
465 "interpret" |
|
466 "invoke" |
463 "show" |
467 "show" |
464 "thus")) |
468 "thus")) |
465 |
469 |
466 (defconst isar-keywords-proof-block |
470 (defconst isar-keywords-proof-block |
467 '("next" |
471 '("next" |