1
;;
2
;; Keyword classification tables for Isabelle/Isar.
3
;; This file was generated by Isabelle/ZF -- DO NOT EDIT!
4
5
;; $Id$
6
7
8
(defconst isar-keywords-major
9
'("\\."
10
"\\.\\."
11
"ML"
12
"ML_command"
13
"ML_setup"
14
"ProofGeneral\\.context_thy_only"
15
"ProofGeneral\\.inform_file_processed"
16
"ProofGeneral\\.inform_file_retracted"
17
"ProofGeneral\\.kill_proof"
18
"ProofGeneral\\.restart"
19
"ProofGeneral\\.try_context_thy_only"
20
"ProofGeneral\\.undo"
21
"also"
22
"apply"
23
"apply_end"
24
"arities"
25
"assume"
26
"axclass"
27
"axioms"
28
"back"
29
"by"
30
"cannot_undo"
31
"case"
32
"cd"
33
"chapter"
34
"classes"
35
"classrel"
36
"clear_undos"
37
"codatatype"
38
"coinductive"
39
"commit"
40
"constdefs"
41
"consts"
42
"consts_code"
43
"context"
44
"corollary"
45
"datatype"
46
"declare"
47
"def"
48
"defaultsort"
49
"defer"
50
"defs"
51
"disable_pr"
52
"done"
53
"enable_pr"
54
"end"
55
"exit"
56
"finally"
57
"fix"
58
"from"
59
"full_prf"
60
"generate_code"
61
"global"
62
"have"
63
"header"
64
"hence"
65
"hide"
66
"inductive"
67
"inductive_cases"
68
"init_toplevel"
69
"instance"
70
"judgment"
71
"kill"
72
"kill_thy"
73
"lemma"
74
"lemmas"
75
"let"
76
"local"
77
"locale"
78
"method_setup"
79
"moreover"
80
"next"
81
"nonterminals"
82
"note"
83
"obtain"
84
"oops"
85
"oracle"
86
"parse_ast_translation"
87
"parse_translation"
88
"pr"
89
"prefer"
90
"presume"
91
"pretty_setmargin"
92
"prf"
93
"primrec"
94
"print_antiquotations"
95
"print_ast_translation"
96
"print_attributes"
97
"print_binds"
98
"print_cases"
99
"print_claset"
100
"print_commands"
101
"print_context"
102
"print_facts"
103
"print_induct_rules"
104
"print_locale"
105
"print_locales"
106
"print_methods"
107
"print_rules"
108
"print_simpset"
109
"print_syntax"
110
"print_tcset"
111
"print_theorems"
112
"print_theory"
113
"print_trans_rules"
114
"print_translation"
115
"proof"
116
"prop"
117
"pwd"
118
"qed"
119
"quit"
120
"redo"
121
"remove_thy"
122
"rep_datatype"
123
"sect"
124
"section"
125
"setup"
126
"show"
127
"sorry"
128
"subsect"
129
"subsection"
130
"subsubsect"
131
"subsubsection"
132
"syntax"
133
"term"
134
"text"
135
"text_raw"
136
"then"
137
"theorem"
138
"theorems"
139
"theory"
140
"thm"
141
"thm_deps"
142
"thms_containing"
143
"thus"
144
"token_translation"
145
"touch_all_thys"
146
"touch_child_thys"
147
"touch_thy"
148
"translations"
149
"txt"
150
"txt_raw"
151
"typ"
152
"typed_print_translation"
153
"typedecl"
154
"types"
155
"types_code"
156
"ultimately"
157
"undo"
158
"undos_proof"
159
"update_thy"
160
"update_thy_only"
161
"use"
162
"use_thy"
163
"use_thy_only"
164
"welcome"
165
"with"
166
"{"
167
"}"))
168
169
(defconst isar-keywords-minor
170
'("and"
171
"assumes"
172
"binder"
173
"case_eqns"
174
"con_defs"
175
"concl"
176
"defines"
177
"domains"
178
"elimination"
179
"files"
180
"fixes"
181
"in"
182
"induction"
183
"infix"
184
"infixl"
185
"infixr"
186
"intros"
187
"is"
188
"monos"
189
"notes"
190
"output"
191
"overloaded"
192
"recursor_eqns"
193
"structure"
194
"type_elims"
195
"type_intros"
196
"uses"
197
"where"))
198
199
(defconst isar-keywords-control
200
'("ProofGeneral\\.context_thy_only"
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
"undos_proof"))
216
217
(defconst isar-keywords-diag
218
'("ML"
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
"welcome"))
266
267
(defconst isar-keywords-theory-begin
268
'("theory"))
269
270
(defconst isar-keywords-theory-switch
271
'("context"))
272
273
(defconst isar-keywords-theory-end
274
'("end"))
275
276
(defconst isar-keywords-theory-heading
277
'("chapter"
278
279
280
"subsubsection"))
281
282
(defconst isar-keywords-theory-decl
283
'("ML_setup"
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
"types_code"))
325
326
(defconst isar-keywords-theory-script
327
'("declare"
328
"inductive_cases"))
329
330
(defconst isar-keywords-theory-goal
331
'("corollary"
332
333
334
"theorem"))
335
336
(defconst isar-keywords-qed
337
338
339
340
341
"sorry"))
342
343
(defconst isar-keywords-qed-block
344
'("qed"))
345
346
(defconst isar-keywords-qed-global
347
'("oops"))
348
349
(defconst isar-keywords-proof-heading
350
'("sect"
351
352
"subsubsect"))
353
354
(defconst isar-keywords-proof-goal
355
'("have"
356
357
358
"thus"))
359
360
(defconst isar-keywords-proof-block
361
'("next"
362
"proof"))
363
364
(defconst isar-keywords-proof-open
365
'("{"))
366
367
(defconst isar-keywords-proof-close
368
'("}"))
369
370
(defconst isar-keywords-proof-chain
371
'("finally"
372
373
374
375
"with"))
376
377
(defconst isar-keywords-proof-decl
378
'("also"
379
380
381
382
383
"txt_raw"))
384
385
(defconst isar-keywords-proof-asm
386
'("assume"
387
388
389
390
"presume"))
391
392
(defconst isar-keywords-proof-asm-goal
393
'("obtain"))
394
395
(defconst isar-keywords-proof-script
396
'("apply"
397
398
399
400
"prefer"))
401
402
(provide 'isar-keywords)