equal
deleted
inserted
replaced
27 "assume" |
27 "assume" |
28 "attribute_setup" |
28 "attribute_setup" |
29 "axiomatization" |
29 "axiomatization" |
30 "axioms" |
30 "axioms" |
31 "back" |
31 "back" |
|
32 "bundle" |
32 "by" |
33 "by" |
33 "cannot_undo" |
34 "cannot_undo" |
34 "case" |
35 "case" |
35 "cd" |
36 "cd" |
36 "chapter" |
37 "chapter" |
74 "hence" |
75 "hence" |
75 "hide_class" |
76 "hide_class" |
76 "hide_const" |
77 "hide_const" |
77 "hide_fact" |
78 "hide_fact" |
78 "hide_type" |
79 "hide_type" |
|
80 "include" |
|
81 "including" |
79 "inductive" |
82 "inductive" |
80 "inductive_cases" |
83 "inductive_cases" |
81 "init_toplevel" |
84 "init_toplevel" |
82 "instance" |
85 "instance" |
83 "instantiation" |
86 "instantiation" |
118 "print_abbrevs" |
121 "print_abbrevs" |
119 "print_antiquotations" |
122 "print_antiquotations" |
120 "print_ast_translation" |
123 "print_ast_translation" |
121 "print_attributes" |
124 "print_attributes" |
122 "print_binds" |
125 "print_binds" |
|
126 "print_bundles" |
123 "print_cases" |
127 "print_cases" |
124 "print_claset" |
128 "print_claset" |
125 "print_classes" |
129 "print_classes" |
126 "print_codesetup" |
130 "print_codesetup" |
127 "print_commands" |
131 "print_commands" |
285 "prf" |
289 "prf" |
286 "print_abbrevs" |
290 "print_abbrevs" |
287 "print_antiquotations" |
291 "print_antiquotations" |
288 "print_attributes" |
292 "print_attributes" |
289 "print_binds" |
293 "print_binds" |
|
294 "print_bundles" |
290 "print_cases" |
295 "print_cases" |
291 "print_claset" |
296 "print_claset" |
292 "print_classes" |
297 "print_classes" |
293 "print_codesetup" |
298 "print_codesetup" |
294 "print_commands" |
299 "print_commands" |
340 "abbreviation" |
345 "abbreviation" |
341 "arities" |
346 "arities" |
342 "attribute_setup" |
347 "attribute_setup" |
343 "axiomatization" |
348 "axiomatization" |
344 "axioms" |
349 "axioms" |
|
350 "bundle" |
345 "class" |
351 "class" |
346 "classes" |
352 "classes" |
347 "classrel" |
353 "classrel" |
348 "codatatype" |
354 "codatatype" |
349 "code_datatype" |
355 "code_datatype" |
456 "with")) |
462 "with")) |
457 |
463 |
458 (defconst isar-keywords-proof-decl |
464 (defconst isar-keywords-proof-decl |
459 '("ML_prf" |
465 '("ML_prf" |
460 "also" |
466 "also" |
|
467 "include" |
|
468 "including" |
461 "let" |
469 "let" |
462 "moreover" |
470 "moreover" |
463 "note" |
471 "note" |
464 "txt" |
472 "txt" |
465 "txt_raw" |
473 "txt_raw" |