equal
deleted
inserted
replaced
71 "hide" |
71 "hide" |
72 "inductive" |
72 "inductive" |
73 "inductive_cases" |
73 "inductive_cases" |
74 "init_toplevel" |
74 "init_toplevel" |
75 "instance" |
75 "instance" |
76 "instantiate" |
|
77 "interpret" |
76 "interpret" |
78 "interpretation" |
77 "interpretation" |
79 "judgment" |
78 "judgment" |
80 "kill" |
79 "kill" |
81 "kill_thy" |
80 "kill_thy" |
190 "begin" |
189 "begin" |
191 "binder" |
190 "binder" |
192 "case_eqns" |
191 "case_eqns" |
193 "con_defs" |
192 "con_defs" |
194 "concl" |
193 "concl" |
|
194 "constrains" |
195 "defines" |
195 "defines" |
196 "domains" |
196 "domains" |
197 "elimination" |
197 "elimination" |
198 "files" |
198 "files" |
199 "fixes" |
199 "fixes" |
411 "ultimately" |
411 "ultimately" |
412 "with")) |
412 "with")) |
413 |
413 |
414 (defconst isar-keywords-proof-decl |
414 (defconst isar-keywords-proof-decl |
415 '("also" |
415 '("also" |
416 "instantiate" |
|
417 "let" |
416 "let" |
418 "moreover" |
417 "moreover" |
419 "note" |
418 "note" |
420 "txt" |
419 "txt" |
421 "txt_raw" |
420 "txt_raw" |