equal
deleted
inserted
replaced
111 "print_induct_rules" |
111 "print_induct_rules" |
112 "print_intros" |
112 "print_intros" |
113 "print_locale" |
113 "print_locale" |
114 "print_locales" |
114 "print_locales" |
115 "print_methods" |
115 "print_methods" |
|
116 "print_registrations" |
116 "print_rules" |
117 "print_rules" |
117 "print_simpset" |
118 "print_simpset" |
118 "print_syntax" |
119 "print_syntax" |
119 "print_tcset" |
120 "print_tcset" |
120 "print_theorems" |
121 "print_theorems" |
129 "quickcheck_params" |
130 "quickcheck_params" |
130 "quit" |
131 "quit" |
131 "realizability" |
132 "realizability" |
132 "realizers" |
133 "realizers" |
133 "redo" |
134 "redo" |
|
135 "registration" |
134 "remove_thy" |
136 "remove_thy" |
135 "rep_datatype" |
137 "rep_datatype" |
136 "sect" |
138 "sect" |
137 "section" |
139 "section" |
138 "setup" |
140 "setup" |
261 "print_induct_rules" |
263 "print_induct_rules" |
262 "print_intros" |
264 "print_intros" |
263 "print_locale" |
265 "print_locale" |
264 "print_locales" |
266 "print_locales" |
265 "print_methods" |
267 "print_methods" |
|
268 "print_registrations" |
266 "print_rules" |
269 "print_rules" |
267 "print_simpset" |
270 "print_simpset" |
268 "print_syntax" |
271 "print_syntax" |
269 "print_tcset" |
272 "print_tcset" |
270 "print_theorems" |
273 "print_theorems" |
360 |
363 |
361 (defconst isar-keywords-theory-goal |
364 (defconst isar-keywords-theory-goal |
362 '("corollary" |
365 '("corollary" |
363 "instance" |
366 "instance" |
364 "lemma" |
367 "lemma" |
|
368 "registration" |
365 "theorem")) |
369 "theorem")) |
366 |
370 |
367 (defconst isar-keywords-qed |
371 (defconst isar-keywords-qed |
368 '("\\." |
372 '("\\." |
369 "\\.\\." |
373 "\\.\\." |