equal
deleted
inserted
replaced
79 "hide" |
79 "hide" |
80 "inductive" |
80 "inductive" |
81 "inductive_cases" |
81 "inductive_cases" |
82 "init_toplevel" |
82 "init_toplevel" |
83 "instance" |
83 "instance" |
84 "instance_proof" |
|
85 "instantiation" |
84 "instantiation" |
86 "interpret" |
85 "interpret" |
87 "interpretation" |
86 "interpretation" |
88 "invoke" |
87 "invoke" |
89 "judgment" |
88 "judgment" |
104 "notation" |
103 "notation" |
105 "note" |
104 "note" |
106 "obtain" |
105 "obtain" |
107 "oops" |
106 "oops" |
108 "oracle" |
107 "oracle" |
|
108 "overloading" |
109 "parse_ast_translation" |
109 "parse_ast_translation" |
110 "parse_translation" |
110 "parse_translation" |
111 "pr" |
111 "pr" |
112 "prefer" |
112 "prefer" |
113 "presume" |
113 "presume" |
376 "no_syntax" |
376 "no_syntax" |
377 "no_translations" |
377 "no_translations" |
378 "nonterminals" |
378 "nonterminals" |
379 "notation" |
379 "notation" |
380 "oracle" |
380 "oracle" |
|
381 "overloading" |
381 "parse_ast_translation" |
382 "parse_ast_translation" |
382 "parse_translation" |
383 "parse_translation" |
383 "primrec" |
384 "primrec" |
384 "print_ast_translation" |
385 "print_ast_translation" |
385 "print_translation" |
386 "print_translation" |
404 '("inductive_cases")) |
405 '("inductive_cases")) |
405 |
406 |
406 (defconst isar-keywords-theory-goal |
407 (defconst isar-keywords-theory-goal |
407 '("corollary" |
408 '("corollary" |
408 "instance" |
409 "instance" |
409 "instance_proof" |
|
410 "interpretation" |
410 "interpretation" |
411 "lemma" |
411 "lemma" |
412 "subclass" |
412 "subclass" |
413 "theorem")) |
413 "theorem")) |
414 |
414 |