equal
deleted
inserted
replaced
72 "inductive" |
72 "inductive" |
73 "inductive_cases" |
73 "inductive_cases" |
74 "init_toplevel" |
74 "init_toplevel" |
75 "instance" |
75 "instance" |
76 "instantiate" |
76 "instantiate" |
|
77 "interpretation" |
77 "judgment" |
78 "judgment" |
78 "kill" |
79 "kill" |
79 "kill_thy" |
80 "kill_thy" |
80 "lemma" |
81 "lemma" |
81 "lemmas" |
82 "lemmas" |
107 "print_commands" |
108 "print_commands" |
108 "print_context" |
109 "print_context" |
109 "print_drafts" |
110 "print_drafts" |
110 "print_facts" |
111 "print_facts" |
111 "print_induct_rules" |
112 "print_induct_rules" |
|
113 "print_interps" |
112 "print_intros" |
114 "print_intros" |
113 "print_locale" |
115 "print_locale" |
114 "print_locales" |
116 "print_locales" |
115 "print_methods" |
117 "print_methods" |
116 "print_registrations" |
|
117 "print_rules" |
118 "print_rules" |
118 "print_simpset" |
119 "print_simpset" |
119 "print_syntax" |
120 "print_syntax" |
120 "print_tcset" |
121 "print_tcset" |
121 "print_theorems" |
122 "print_theorems" |
130 "quickcheck_params" |
131 "quickcheck_params" |
131 "quit" |
132 "quit" |
132 "realizability" |
133 "realizability" |
133 "realizers" |
134 "realizers" |
134 "redo" |
135 "redo" |
135 "registration" |
|
136 "remove_thy" |
136 "remove_thy" |
137 "rep_datatype" |
137 "rep_datatype" |
138 "sect" |
138 "sect" |
139 "section" |
139 "section" |
140 "setup" |
140 "setup" |
259 "print_commands" |
259 "print_commands" |
260 "print_context" |
260 "print_context" |
261 "print_drafts" |
261 "print_drafts" |
262 "print_facts" |
262 "print_facts" |
263 "print_induct_rules" |
263 "print_induct_rules" |
|
264 "print_interps" |
264 "print_intros" |
265 "print_intros" |
265 "print_locale" |
266 "print_locale" |
266 "print_locales" |
267 "print_locales" |
267 "print_methods" |
268 "print_methods" |
268 "print_registrations" |
|
269 "print_rules" |
269 "print_rules" |
270 "print_simpset" |
270 "print_simpset" |
271 "print_syntax" |
271 "print_syntax" |
272 "print_tcset" |
272 "print_tcset" |
273 "print_theorems" |
273 "print_theorems" |
362 "inductive_cases")) |
362 "inductive_cases")) |
363 |
363 |
364 (defconst isar-keywords-theory-goal |
364 (defconst isar-keywords-theory-goal |
365 '("corollary" |
365 '("corollary" |
366 "instance" |
366 "instance" |
|
367 "interpretation" |
367 "lemma" |
368 "lemma" |
368 "registration" |
|
369 "theorem")) |
369 "theorem")) |
370 |
370 |
371 (defconst isar-keywords-qed |
371 (defconst isar-keywords-qed |
372 '("\\." |
372 '("\\." |
373 "\\.\\." |
373 "\\.\\." |