equal
deleted
inserted
replaced
72 "inductive" |
72 "inductive" |
73 "inductive_cases" |
73 "inductive_cases" |
74 "init_toplevel" |
74 "init_toplevel" |
75 "instance" |
75 "instance" |
76 "instantiate" |
76 "instantiate" |
|
77 "interpret" |
77 "interpretation" |
78 "interpretation" |
78 "judgment" |
79 "judgment" |
79 "kill" |
80 "kill" |
80 "kill_thy" |
81 "kill_thy" |
81 "lemma" |
82 "lemma" |
387 "subsubsect")) |
388 "subsubsect")) |
388 |
389 |
389 (defconst isar-keywords-proof-goal |
390 (defconst isar-keywords-proof-goal |
390 '("have" |
391 '("have" |
391 "hence" |
392 "hence" |
|
393 "interpret" |
392 "show" |
394 "show" |
393 "thus")) |
395 "thus")) |
394 |
396 |
395 (defconst isar-keywords-proof-block |
397 (defconst isar-keywords-proof-block |
396 '("next" |
398 '("next" |