equal
deleted
inserted
replaced
147 "no_notation" |
147 "no_notation" |
148 "no_syntax" |
148 "no_syntax" |
149 "no_translations" |
149 "no_translations" |
150 "no_type_notation" |
150 "no_type_notation" |
151 "nominal_datatype" |
151 "nominal_datatype" |
|
152 "nominal_function" |
152 "nominal_inductive" |
153 "nominal_inductive" |
153 "nominal_inductive2" |
154 "nominal_inductive2" |
154 "nominal_primrec" |
155 "nominal_primrec" |
|
156 "nominal_termination" |
155 "nonterminal" |
157 "nonterminal" |
156 "notation" |
158 "notation" |
157 "note" |
159 "note" |
158 "notepad" |
160 "notepad" |
159 "obtain" |
161 "obtain" |
313 "assumes" |
315 "assumes" |
314 "attach" |
316 "attach" |
315 "avoids" |
317 "avoids" |
316 "begin" |
318 "begin" |
317 "binder" |
319 "binder" |
|
320 "binds" |
318 "checking" |
321 "checking" |
319 "class_instance" |
322 "class_instance" |
320 "class_relation" |
323 "class_relation" |
321 "code_module" |
324 "code_module" |
322 "congs" |
325 "congs" |
611 "functor" |
614 "functor" |
612 "instance" |
615 "instance" |
613 "interpretation" |
616 "interpretation" |
614 "lemma" |
617 "lemma" |
615 "lift_definition" |
618 "lift_definition" |
|
619 "nominal_function" |
616 "nominal_inductive" |
620 "nominal_inductive" |
617 "nominal_inductive2" |
621 "nominal_inductive2" |
618 "nominal_primrec" |
622 "nominal_primrec" |
|
623 "nominal_termination" |
619 "pcpodef" |
624 "pcpodef" |
620 "permanent_interpretation" |
625 "permanent_interpretation" |
621 "primcorecursive" |
626 "primcorecursive" |
622 "quotient_definition" |
627 "quotient_definition" |
623 "quotient_type" |
628 "quotient_type" |