equal
deleted
inserted
replaced
33 "back" |
33 "back" |
34 "boogie_end" |
34 "boogie_end" |
35 "boogie_open" |
35 "boogie_open" |
36 "boogie_status" |
36 "boogie_status" |
37 "boogie_vc" |
37 "boogie_vc" |
|
38 "bundle" |
38 "by" |
39 "by" |
39 "cannot_undo" |
40 "cannot_undo" |
40 "case" |
41 "case" |
41 "cd" |
42 "cd" |
42 "chapter" |
43 "chapter" |
106 "hide_class" |
107 "hide_class" |
107 "hide_const" |
108 "hide_const" |
108 "hide_fact" |
109 "hide_fact" |
109 "hide_type" |
110 "hide_type" |
110 "import_tptp" |
111 "import_tptp" |
|
112 "include" |
|
113 "including" |
111 "inductive" |
114 "inductive" |
112 "inductive_cases" |
115 "inductive_cases" |
113 "inductive_set" |
116 "inductive_set" |
114 "inductive_simps" |
117 "inductive_simps" |
115 "init_toplevel" |
118 "init_toplevel" |
160 "print_abbrevs" |
163 "print_abbrevs" |
161 "print_antiquotations" |
164 "print_antiquotations" |
162 "print_ast_translation" |
165 "print_ast_translation" |
163 "print_attributes" |
166 "print_attributes" |
164 "print_binds" |
167 "print_binds" |
|
168 "print_bundles" |
165 "print_cases" |
169 "print_cases" |
166 "print_claset" |
170 "print_claset" |
167 "print_classes" |
171 "print_classes" |
168 "print_codeproc" |
172 "print_codeproc" |
169 "print_codesetup" |
173 "print_codesetup" |
370 "prf" |
374 "prf" |
371 "print_abbrevs" |
375 "print_abbrevs" |
372 "print_antiquotations" |
376 "print_antiquotations" |
373 "print_attributes" |
377 "print_attributes" |
374 "print_binds" |
378 "print_binds" |
|
379 "print_bundles" |
375 "print_cases" |
380 "print_cases" |
376 "print_claset" |
381 "print_claset" |
377 "print_classes" |
382 "print_classes" |
378 "print_codeproc" |
383 "print_codeproc" |
379 "print_codesetup" |
384 "print_codesetup" |
444 "attribute_setup" |
449 "attribute_setup" |
445 "axiomatization" |
450 "axiomatization" |
446 "axioms" |
451 "axioms" |
447 "boogie_end" |
452 "boogie_end" |
448 "boogie_open" |
453 "boogie_open" |
|
454 "bundle" |
449 "class" |
455 "class" |
450 "classes" |
456 "classes" |
451 "classrel" |
457 "classrel" |
452 "code_abort" |
458 "code_abort" |
453 "code_class" |
459 "code_class" |
611 "with")) |
617 "with")) |
612 |
618 |
613 (defconst isar-keywords-proof-decl |
619 (defconst isar-keywords-proof-decl |
614 '("ML_prf" |
620 '("ML_prf" |
615 "also" |
621 "also" |
|
622 "include" |
|
623 "including" |
616 "let" |
624 "let" |
617 "moreover" |
625 "moreover" |
618 "note" |
626 "note" |
619 "txt" |
627 "txt" |
620 "txt_raw" |
628 "txt_raw" |