equal
deleted
inserted
replaced
160 "quit" |
160 "quit" |
161 "realizability" |
161 "realizability" |
162 "realizers" |
162 "realizers" |
163 "remove_thy" |
163 "remove_thy" |
164 "rep_datatype" |
164 "rep_datatype" |
|
165 "schematic_corollary" |
|
166 "schematic_lemma" |
|
167 "schematic_theorem" |
165 "sect" |
168 "sect" |
166 "section" |
169 "section" |
167 "setup" |
170 "setup" |
168 "show" |
171 "show" |
169 "simproc_setup" |
172 "simproc_setup" |
423 (defconst isar-keywords-theory-goal |
426 (defconst isar-keywords-theory-goal |
424 '("corollary" |
427 '("corollary" |
425 "instance" |
428 "instance" |
426 "interpretation" |
429 "interpretation" |
427 "lemma" |
430 "lemma" |
|
431 "schematic_corollary" |
|
432 "schematic_lemma" |
|
433 "schematic_theorem" |
428 "subclass" |
434 "subclass" |
429 "sublocale" |
435 "sublocale" |
430 "theorem")) |
436 "theorem")) |
431 |
437 |
432 (defconst isar-keywords-qed |
438 (defconst isar-keywords-qed |