equal
deleted
inserted
replaced
151 "print_induct_rules" |
151 "print_induct_rules" |
152 "print_interps" |
152 "print_interps" |
153 "print_locale" |
153 "print_locale" |
154 "print_locales" |
154 "print_locales" |
155 "print_methods" |
155 "print_methods" |
|
156 "print_options" |
156 "print_rules" |
157 "print_rules" |
157 "print_simpset" |
158 "print_simpset" |
158 "print_statement" |
159 "print_statement" |
159 "print_syntax" |
160 "print_syntax" |
160 "print_theorems" |
161 "print_theorems" |
219 "ultimately" |
220 "ultimately" |
220 "undo" |
221 "undo" |
221 "undos_proof" |
222 "undos_proof" |
222 "unfolding" |
223 "unfolding" |
223 "update_thy" |
224 "update_thy" |
224 "update_thy_only" |
|
225 "use" |
225 "use" |
226 "use_thy" |
226 "use_thy" |
227 "use_thy_only" |
|
228 "using" |
227 "using" |
229 "value" |
228 "value" |
230 "welcome" |
229 "welcome" |
231 "with" |
230 "with" |
232 "{" |
231 "{" |
345 "print_induct_rules" |
344 "print_induct_rules" |
346 "print_interps" |
345 "print_interps" |
347 "print_locale" |
346 "print_locale" |
348 "print_locales" |
347 "print_locales" |
349 "print_methods" |
348 "print_methods" |
|
349 "print_options" |
350 "print_rules" |
350 "print_rules" |
351 "print_simpset" |
351 "print_simpset" |
352 "print_statement" |
352 "print_statement" |
353 "print_syntax" |
353 "print_syntax" |
354 "print_theorems" |
354 "print_theorems" |
367 "touch_all_thys" |
367 "touch_all_thys" |
368 "touch_child_thys" |
368 "touch_child_thys" |
369 "touch_thy" |
369 "touch_thy" |
370 "typ" |
370 "typ" |
371 "update_thy" |
371 "update_thy" |
372 "update_thy_only" |
|
373 "use" |
372 "use" |
374 "use_thy" |
373 "use_thy" |
375 "use_thy_only" |
|
376 "value" |
374 "value" |
377 "welcome")) |
375 "welcome")) |
378 |
376 |
379 (defconst isar-keywords-theory-begin |
377 (defconst isar-keywords-theory-begin |
380 '("theory")) |
378 '("theory")) |