equal
deleted
inserted
replaced
65 "find_theorems" |
65 "find_theorems" |
66 "fix" |
66 "fix" |
67 "from" |
67 "from" |
68 "full_prf" |
68 "full_prf" |
69 "global" |
69 "global" |
|
70 "guess" |
70 "have" |
71 "have" |
71 "header" |
72 "header" |
72 "hence" |
73 "hence" |
73 "hide" |
74 "hide" |
74 "inductive" |
75 "inductive" |
434 "def" |
435 "def" |
435 "fix" |
436 "fix" |
436 "presume")) |
437 "presume")) |
437 |
438 |
438 (defconst isar-keywords-proof-asm-goal |
439 (defconst isar-keywords-proof-asm-goal |
439 '("obtain")) |
440 '("guess" |
|
441 "obtain")) |
440 |
442 |
441 (defconst isar-keywords-proof-script |
443 (defconst isar-keywords-proof-script |
442 '("apply" |
444 '("apply" |
443 "apply_end" |
445 "apply_end" |
444 "back" |
446 "back" |