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
"using"
165
"welcome"
166
"with"
167
"{"
168
"}"))
169
170
(defconst isar-keywords-minor
171
'("and"
172
"assumes"
173
"binder"
174
"case_eqns"
175
"con_defs"
176
"concl"
177
"defines"
178
"domains"
179
"elimination"
180
"files"
181
"fixes"
182
"in"
183
"induction"
184
"infix"
185
"infixl"
186
"infixr"
187
"intros"
188
"is"
189
"monos"
190
"notes"
191
"output"
192
"overloaded"
193
"recursor_eqns"
194
"shows"
195
"structure"
196
"type_elims"
197
"type_intros"
198
"uses"
199
"where"))
200
201
(defconst isar-keywords-control
202
'("ProofGeneral\\.context_thy_only"
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
"undos_proof"))
218
219
(defconst isar-keywords-diag
220
'("ML"
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
266
267
"welcome"))
268
269
(defconst isar-keywords-theory-begin
270
'("theory"))
271
272
(defconst isar-keywords-theory-switch
273
'("context"))
274
275
(defconst isar-keywords-theory-end
276
'("end"))
277
278
(defconst isar-keywords-theory-heading
279
'("chapter"
280
281
282
"subsubsection"))
283
284
(defconst isar-keywords-theory-decl
285
'("ML_setup"
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
325
326
"types_code"))
327
328
(defconst isar-keywords-theory-script
329
'("declare"
330
"inductive_cases"))
331
332
(defconst isar-keywords-theory-goal
333
'("corollary"
334
335
336
"theorem"))
337
338
(defconst isar-keywords-qed
339
340
341
342
343
"sorry"))
344
345
(defconst isar-keywords-qed-block
346
'("qed"))
347
348
(defconst isar-keywords-qed-global
349
'("oops"))
350
351
(defconst isar-keywords-proof-heading
352
'("sect"
353
354
"subsubsect"))
355
356
(defconst isar-keywords-proof-goal
357
'("have"
358
359
360
"thus"))
361
362
(defconst isar-keywords-proof-block
363
'("next"
364
"proof"))
365
366
(defconst isar-keywords-proof-open
367
'("{"))
368
369
(defconst isar-keywords-proof-close
370
'("}"))
371
372
(defconst isar-keywords-proof-chain
373
'("finally"
374
375
376
377
"with"))
378
379
(defconst isar-keywords-proof-decl
380
'("also"
381
382
383
384
385
386
"using"))
387
388
(defconst isar-keywords-proof-asm
389
'("assume"
390
391
392
393
"presume"))
394
395
(defconst isar-keywords-proof-asm-goal
396
'("obtain"))
397
398
(defconst isar-keywords-proof-script
399
'("apply"
400
401
402
403
"prefer"))
404
405
(provide 'isar-keywords)