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
"coinductive"
38
"commit"
39
"constdefs"
40
"consts"
41
"consts_code"
42
"context"
43
"corollary"
44
"declare"
45
"def"
46
"defaultsort"
47
"defer"
48
"defs"
49
"disable_pr"
50
"done"
51
"enable_pr"
52
"end"
53
"exit"
54
"finally"
55
"fix"
56
"from"
57
"full_prf"
58
"generate_code"
59
"global"
60
"have"
61
"header"
62
"hence"
63
"hide"
64
"inductive"
65
"inductive_cases"
66
"init_toplevel"
67
"instance"
68
"judgment"
69
"kill"
70
"kill_thy"
71
"lemma"
72
"lemmas"
73
"let"
74
"local"
75
"locale"
76
"method_setup"
77
"moreover"
78
"next"
79
"nonterminals"
80
"note"
81
"obtain"
82
"oops"
83
"oracle"
84
"parse_ast_translation"
85
"parse_translation"
86
"pr"
87
"prefer"
88
"presume"
89
"pretty_setmargin"
90
"prf"
91
"print_antiquotations"
92
"print_ast_translation"
93
"print_attributes"
94
"print_binds"
95
"print_cases"
96
"print_claset"
97
"print_commands"
98
"print_context"
99
"print_facts"
100
"print_induct_rules"
101
"print_locale"
102
"print_locales"
103
"print_methods"
104
"print_simpset"
105
"print_syntax"
106
"print_theorems"
107
"print_theory"
108
"print_trans_rules"
109
"print_translation"
110
"proof"
111
"prop"
112
"pwd"
113
"qed"
114
"quit"
115
"redo"
116
"remove_thy"
117
"sect"
118
"section"
119
"setup"
120
"show"
121
"sorry"
122
"subsect"
123
"subsection"
124
"subsubsect"
125
"subsubsection"
126
"syntax"
127
"term"
128
"text"
129
"text_raw"
130
"then"
131
"theorem"
132
"theorems"
133
"theory"
134
"thm"
135
"thm_deps"
136
"thms_containing"
137
"thus"
138
"token_translation"
139
"touch_all_thys"
140
"touch_child_thys"
141
"touch_thy"
142
"translations"
143
"txt"
144
"txt_raw"
145
"typ"
146
"typed_print_translation"
147
"typedecl"
148
"types"
149
"types_code"
150
"ultimately"
151
"undo"
152
"undos_proof"
153
"update_thy"
154
"update_thy_only"
155
"use"
156
"use_thy"
157
"use_thy_only"
158
"welcome"
159
"with"
160
"{"
161
"}"))
162
163
(defconst isar-keywords-minor
164
'("and"
165
"assumes"
166
"binder"
167
"con_defs"
168
"concl"
169
"defines"
170
"domains"
171
"files"
172
"fixes"
173
"in"
174
"infix"
175
"infixl"
176
"infixr"
177
"intros"
178
"is"
179
"monos"
180
"notes"
181
"output"
182
"overloaded"
183
"structure"
184
"type_elims"
185
"type_intros"
186
"uses"
187
"where"))
188
189
(defconst isar-keywords-control
190
'("ProofGeneral\\.context_thy_only"
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
"undos_proof"))
206
207
(defconst isar-keywords-diag
208
'("ML"
209
210
211
212
213
214
215
216
217
218
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
"welcome"))
254
255
(defconst isar-keywords-theory-begin
256
'("theory"))
257
258
(defconst isar-keywords-theory-switch
259
'("context"))
260
261
(defconst isar-keywords-theory-end
262
'("end"))
263
264
(defconst isar-keywords-theory-heading
265
'("chapter"
266
267
268
"subsubsection"))
269
270
(defconst isar-keywords-theory-decl
271
'("ML_setup"
272
273
274
275
276
277
278
279
280
281
282
283
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
"types_code"))
309
310
(defconst isar-keywords-theory-script
311
'("declare"
312
"inductive_cases"))
313
314
(defconst isar-keywords-theory-goal
315
'("corollary"
316
317
318
"theorem"))
319
320
(defconst isar-keywords-qed
321
322
323
324
325
"sorry"))
326
327
(defconst isar-keywords-qed-block
328
'("qed"))
329
330
(defconst isar-keywords-qed-global
331
'("oops"))
332
333
(defconst isar-keywords-proof-heading
334
'("sect"
335
336
"subsubsect"))
337
338
(defconst isar-keywords-proof-goal
339
'("have"
340
341
342
"thus"))
343
344
(defconst isar-keywords-proof-block
345
'("next"
346
"proof"))
347
348
(defconst isar-keywords-proof-open
349
'("{"))
350
351
(defconst isar-keywords-proof-close
352
'("}"))
353
354
(defconst isar-keywords-proof-chain
355
'("finally"
356
357
358
359
"with"))
360
361
(defconst isar-keywords-proof-decl
362
'("also"
363
364
365
366
367
"txt_raw"))
368
369
(defconst isar-keywords-proof-asm
370
'("assume"
371
372
373
374
"presume"))
375
376
(defconst isar-keywords-proof-asm-goal
377
'("obtain"))
378
379
(defconst isar-keywords-proof-script
380
'("apply"
381
382
383
384
"prefer"))
385
386
(provide 'isar-keywords)