equal
deleted
inserted
replaced
36 "chapter" |
36 "chapter" |
37 "class" |
37 "class" |
38 "class_deps" |
38 "class_deps" |
39 "classes" |
39 "classes" |
40 "classrel" |
40 "classrel" |
41 "code_abstype" |
|
42 "code_axioms" |
|
43 "code_class" |
41 "code_class" |
44 "code_const" |
42 "code_const" |
45 "code_datatype" |
43 "code_datatype" |
46 "code_deps" |
44 "code_deps" |
47 "code_instance" |
45 "code_instance" |
48 "code_library" |
46 "code_library" |
49 "code_module" |
47 "code_module" |
50 "code_modulename" |
48 "code_modulename" |
51 "code_moduleprolog" |
49 "code_moduleprolog" |
52 "code_monad" |
50 "code_monad" |
|
51 "code_props" |
53 "code_reserved" |
52 "code_reserved" |
54 "code_thms" |
53 "code_thms" |
55 "code_type" |
54 "code_type" |
56 "coinductive" |
55 "coinductive" |
57 "coinductive_set" |
56 "coinductive_set" |
98 "inductive" |
97 "inductive" |
99 "inductive_cases" |
98 "inductive_cases" |
100 "inductive_set" |
99 "inductive_set" |
101 "init_toplevel" |
100 "init_toplevel" |
102 "instance" |
101 "instance" |
|
102 "instance_proof" |
|
103 "instantiation" |
103 "interpret" |
104 "interpret" |
104 "interpretation" |
105 "interpretation" |
105 "invoke" |
106 "invoke" |
106 "judgment" |
107 "judgment" |
107 "kill" |
108 "kill" |
384 "axiomatization" |
385 "axiomatization" |
385 "axioms" |
386 "axioms" |
386 "class" |
387 "class" |
387 "classes" |
388 "classes" |
388 "classrel" |
389 "classrel" |
389 "code_abstype" |
|
390 "code_axioms" |
|
391 "code_class" |
390 "code_class" |
392 "code_const" |
391 "code_const" |
393 "code_datatype" |
392 "code_datatype" |
394 "code_instance" |
393 "code_instance" |
395 "code_library" |
394 "code_library" |
396 "code_module" |
395 "code_module" |
397 "code_modulename" |
396 "code_modulename" |
398 "code_moduleprolog" |
397 "code_moduleprolog" |
399 "code_monad" |
398 "code_monad" |
|
399 "code_props" |
400 "code_reserved" |
400 "code_reserved" |
401 "code_type" |
401 "code_type" |
402 "coinductive" |
402 "coinductive" |
403 "coinductive_set" |
403 "coinductive_set" |
404 "constdefs" |
404 "constdefs" |
419 "fun" |
419 "fun" |
420 "global" |
420 "global" |
421 "hide" |
421 "hide" |
422 "inductive" |
422 "inductive" |
423 "inductive_set" |
423 "inductive_set" |
|
424 "instantiation" |
424 "judgment" |
425 "judgment" |
425 "lemmas" |
426 "lemmas" |
426 "local" |
427 "local" |
427 "locale" |
428 "locale" |
428 "method_setup" |
429 "method_setup" |
463 (defconst isar-keywords-theory-goal |
464 (defconst isar-keywords-theory-goal |
464 '("ax_specification" |
465 '("ax_specification" |
465 "corollary" |
466 "corollary" |
466 "function" |
467 "function" |
467 "instance" |
468 "instance" |
|
469 "instance_proof" |
468 "interpretation" |
470 "interpretation" |
469 "lemma" |
471 "lemma" |
470 "nominal_inductive" |
472 "nominal_inductive" |
471 "nominal_primrec" |
473 "nominal_primrec" |
472 "recdef_tc" |
474 "recdef_tc" |