equal
deleted
inserted
replaced
59 "code_library" |
59 "code_library" |
60 "code_module" |
60 "code_module" |
61 "code_modulename" |
61 "code_modulename" |
62 "code_monad" |
62 "code_monad" |
63 "code_pred" |
63 "code_pred" |
|
64 "code_reflect" |
64 "code_reserved" |
65 "code_reserved" |
65 "code_thms" |
66 "code_thms" |
66 "code_type" |
67 "code_type" |
67 "coinductive" |
68 "coinductive" |
68 "coinductive_set" |
69 "coinductive_set" |
74 "corollary" |
75 "corollary" |
75 "datatype" |
76 "datatype" |
76 "declaration" |
77 "declaration" |
77 "declare" |
78 "declare" |
78 "def" |
79 "def" |
79 "defaultsort" |
80 "default_sort" |
80 "defer" |
81 "defer" |
81 "defer_recdef" |
82 "defer_recdef" |
82 "definition" |
83 "definition" |
83 "defs" |
84 "defs" |
84 "disable_pr" |
85 "disable_pr" |
104 "guess" |
105 "guess" |
105 "have" |
106 "have" |
106 "header" |
107 "header" |
107 "help" |
108 "help" |
108 "hence" |
109 "hence" |
109 "hide" |
110 "hide_class" |
|
111 "hide_const" |
|
112 "hide_fact" |
|
113 "hide_type" |
110 "inductive" |
114 "inductive" |
111 "inductive_cases" |
115 "inductive_cases" |
112 "inductive_set" |
116 "inductive_set" |
113 "init_toplevel" |
117 "init_toplevel" |
114 "instance" |
118 "instance" |
203 "record" |
207 "record" |
204 "refute" |
208 "refute" |
205 "refute_params" |
209 "refute_params" |
206 "remove_thy" |
210 "remove_thy" |
207 "rep_datatype" |
211 "rep_datatype" |
|
212 "repdef" |
|
213 "schematic_corollary" |
|
214 "schematic_lemma" |
|
215 "schematic_theorem" |
208 "sect" |
216 "sect" |
209 "section" |
217 "section" |
210 "setup" |
218 "setup" |
211 "show" |
219 "show" |
212 "simproc_setup" |
220 "simproc_setup" |
213 "sledgehammer" |
221 "sledgehammer" |
|
222 "sledgehammer_params" |
|
223 "smt_status" |
214 "sorry" |
224 "sorry" |
215 "specification" |
225 "specification" |
216 "subclass" |
226 "subclass" |
217 "sublocale" |
227 "sublocale" |
218 "subsect" |
228 "subsect" |
431 "code_instance" |
441 "code_instance" |
432 "code_library" |
442 "code_library" |
433 "code_module" |
443 "code_module" |
434 "code_modulename" |
444 "code_modulename" |
435 "code_monad" |
445 "code_monad" |
|
446 "code_reflect" |
436 "code_reserved" |
447 "code_reserved" |
437 "code_type" |
448 "code_type" |
438 "coinductive" |
449 "coinductive" |
439 "coinductive_set" |
450 "coinductive_set" |
440 "constdefs" |
451 "constdefs" |
452 "extract" |
463 "extract" |
453 "extract_type" |
464 "extract_type" |
454 "finalconsts" |
465 "finalconsts" |
455 "fun" |
466 "fun" |
456 "global" |
467 "global" |
457 "hide" |
468 "hide_class" |
|
469 "hide_const" |
|
470 "hide_fact" |
|
471 "hide_type" |
458 "inductive" |
472 "inductive" |
459 "inductive_set" |
473 "inductive_set" |
460 "instantiation" |
474 "instantiation" |
461 "judgment" |
475 "judgment" |
462 "lemmas" |
476 "lemmas" |
485 "recdef" |
499 "recdef" |
486 "record" |
500 "record" |
487 "refute_params" |
501 "refute_params" |
488 "setup" |
502 "setup" |
489 "simproc_setup" |
503 "simproc_setup" |
|
504 "sledgehammer_params" |
|
505 "statespace" |
490 "syntax" |
506 "syntax" |
491 "text" |
507 "text" |
492 "text_raw" |
508 "text_raw" |
493 "theorems" |
509 "theorems" |
494 "translations" |
510 "translations" |
514 "nominal_primrec" |
530 "nominal_primrec" |
515 "prove" |
531 "prove" |
516 "quotient_type" |
532 "quotient_type" |
517 "recdef_tc" |
533 "recdef_tc" |
518 "rep_datatype" |
534 "rep_datatype" |
|
535 "schematic_corollary" |
|
536 "schematic_lemma" |
|
537 "schematic_theorem" |
519 "specification" |
538 "specification" |
520 "subclass" |
539 "subclass" |
521 "sublocale" |
540 "sublocale" |
522 "termination" |
541 "termination" |
523 "theorem" |
542 "theorem" |