equal
deleted
inserted
replaced
104 "inductive" |
104 "inductive" |
105 "inductive_cases" |
105 "inductive_cases" |
106 "inductive_set" |
106 "inductive_set" |
107 "init_toplevel" |
107 "init_toplevel" |
108 "instance" |
108 "instance" |
109 "instance_proof" |
|
110 "instantiation" |
109 "instantiation" |
111 "interpret" |
110 "interpret" |
112 "interpretation" |
111 "interpretation" |
113 "invoke" |
112 "invoke" |
114 "judgment" |
113 "judgment" |
133 "notation" |
132 "notation" |
134 "note" |
133 "note" |
135 "obtain" |
134 "obtain" |
136 "oops" |
135 "oops" |
137 "oracle" |
136 "oracle" |
|
137 "overloading" |
138 "parse_ast_translation" |
138 "parse_ast_translation" |
139 "parse_translation" |
139 "parse_translation" |
140 "pcpodef" |
140 "pcpodef" |
141 "pr" |
141 "pr" |
142 "prefer" |
142 "prefer" |
464 "no_translations" |
464 "no_translations" |
465 "nominal_datatype" |
465 "nominal_datatype" |
466 "nonterminals" |
466 "nonterminals" |
467 "notation" |
467 "notation" |
468 "oracle" |
468 "oracle" |
|
469 "overloading" |
469 "parse_ast_translation" |
470 "parse_ast_translation" |
470 "parse_translation" |
471 "parse_translation" |
471 "primrec" |
472 "primrec" |
472 "print_ast_translation" |
473 "print_ast_translation" |
473 "print_translation" |
474 "print_translation" |
499 '("ax_specification" |
500 '("ax_specification" |
500 "corollary" |
501 "corollary" |
501 "cpodef" |
502 "cpodef" |
502 "function" |
503 "function" |
503 "instance" |
504 "instance" |
504 "instance_proof" |
|
505 "interpretation" |
505 "interpretation" |
506 "lemma" |
506 "lemma" |
507 "nominal_inductive" |
507 "nominal_inductive" |
508 "nominal_primrec" |
508 "nominal_primrec" |
509 "pcpodef" |
509 "pcpodef" |