| changeset 18541 | 00890455e95f |
| parent 18520 | 428c79932b53 |
| child 18552 | 30911da9fb27 |
| 18540:7b6f57406b1b | 18541:00890455e95f |
|---|---|
181 "types" |
181 "types" |
182 "types_code" |
182 "types_code" |
183 "ultimately" |
183 "ultimately" |
184 "undo" |
184 "undo" |
185 "undos_proof" |
185 "undos_proof" |
186 "unfolding" |
|
186 "update_thy" |
187 "update_thy" |
187 "update_thy_only" |
188 "update_thy_only" |
188 "use" |
189 "use" |
189 "use_thy" |
190 "use_thy" |
190 "use_thy_only" |
191 "use_thy_only" |
197 |
198 |
198 (defconst isar-keywords-minor |
199 (defconst isar-keywords-minor |
199 '("advanced" |
200 '("advanced" |
200 "and" |
201 "and" |
201 "assumes" |
202 "assumes" |
202 "atom" |
|
203 "attach" |
203 "attach" |
204 "begin" |
204 "begin" |
205 "binder" |
205 "binder" |
206 "case_eqns" |
206 "case_eqns" |
207 "con_defs" |
207 "con_defs" |
448 "let" |
448 "let" |
449 "moreover" |
449 "moreover" |
450 "note" |
450 "note" |
451 "txt" |
451 "txt" |
452 "txt_raw" |
452 "txt_raw" |
453 "unfolding" |
|
453 "using")) |
454 "using")) |
454 |
455 |
455 (defconst isar-keywords-proof-asm |
456 (defconst isar-keywords-proof-asm |
456 '("assume" |
457 '("assume" |
457 "case" |
458 "case" |