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
"extract"
57
"extract_type"
58
"finalconsts"
59
"finally"
60
"fix"
61
"from"
62
"full_prf"
63
"generate_code"
64
"global"
65
"have"
66
"header"
67
"hence"
68
"hide"
69
"inductive"
70
"inductive_cases"
71
"init_toplevel"
72
"instance"
73
"instantiate"
74
"judgment"
75
"kill"
76
"kill_thy"
77
"lemma"
78
"lemmas"
79
"let"
80
"local"
81
"locale"
82
"method_setup"
83
"moreover"
84
"next"
85
"nonterminals"
86
"note"
87
"obtain"
88
"oops"
89
"oracle"
90
"parse_ast_translation"
91
"parse_translation"
92
"pr"
93
"prefer"
94
"presume"
95
"pretty_setmargin"
96
"prf"
97
"primrec"
98
"print_antiquotations"
99
"print_ast_translation"
100
"print_attributes"
101
"print_binds"
102
"print_cases"
103
"print_claset"
104
"print_commands"
105
"print_context"
106
"print_facts"
107
"print_induct_rules"
108
"print_intros"
109
"print_locale"
110
"print_locales"
111
"print_methods"
112
"print_rules"
113
"print_simpset"
114
"print_syntax"
115
"print_tcset"
116
"print_theorems"
117
"print_theory"
118
"print_trans_rules"
119
"print_translation"
120
"proof"
121
"prop"
122
"pwd"
123
"qed"
124
"quickcheck"
125
"quickcheck_params"
126
"quit"
127
"realizability"
128
"realizers"
129
"redo"
130
"remove_thy"
131
"rep_datatype"
132
"sect"
133
"section"
134
"setup"
135
"show"
136
"sorry"
137
"subsect"
138
"subsection"
139
"subsubsect"
140
"subsubsection"
141
"syntax"
142
"term"
143
"text"
144
"text_raw"
145
"then"
146
"theorem"
147
"theorems"
148
"theory"
149
"thm"
150
"thm_deps"
151
"thms_containing"
152
"thus"
153
"token_translation"
154
"touch_all_thys"
155
"touch_child_thys"
156
"touch_thy"
157
"translations"
158
"txt"
159
"txt_raw"
160
"typ"
161
"typed_print_translation"
162
"typedecl"
163
"types"
164
"types_code"
165
"ultimately"
166
"undo"
167
"undos_proof"
168
"update_thy"
169
"update_thy_only"
170
"use"
171
"use_thy"
172
"use_thy_only"
173
"using"
174
"welcome"
175
"with"
176
"{"
177
"}"))
178
179
(defconst isar-keywords-minor
180
'("advanced"
181
"and"
182
"assumes"
183
"binder"
184
"case_eqns"
185
"con_defs"
186
"concl"
187
"defines"
188
"domains"
189
"elimination"
190
"files"
191
"fixes"
192
"in"
193
"includes"
194
"induction"
195
"infix"
196
"infixl"
197
"infixr"
198
"intros"
199
"is"
200
"monos"
201
"notes"
202
"open"
203
"output"
204
"overloaded"
205
"recursor_eqns"
206
"shows"
207
"structure"
208
"type_elims"
209
"type_intros"
210
"where"))
211
212
(defconst isar-keywords-control
213
'("ProofGeneral\\.context_thy_only"
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
"undos_proof"))
229
230
(defconst isar-keywords-diag
231
'("ML"
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
268
269
270
271
272
273
274
275
276
277
278
279
280
"welcome"))
281
282
(defconst isar-keywords-theory-begin
283
'("theory"))
284
285
(defconst isar-keywords-theory-switch
286
'("context"))
287
288
(defconst isar-keywords-theory-end
289
'("end"))
290
291
(defconst isar-keywords-theory-heading
292
'("chapter"
293
294
295
"subsubsection"))
296
297
(defconst isar-keywords-theory-decl
298
'("ML_setup"
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
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
"types_code"))
346
347
(defconst isar-keywords-theory-script
348
'("declare"
349
"inductive_cases"))
350
351
(defconst isar-keywords-theory-goal
352
'("corollary"
353
354
355
"theorem"))
356
357
(defconst isar-keywords-qed
358
359
360
361
362
"sorry"))
363
364
(defconst isar-keywords-qed-block
365
'("qed"))
366
367
(defconst isar-keywords-qed-global
368
'("oops"))
369
370
(defconst isar-keywords-proof-heading
371
'("sect"
372
373
"subsubsect"))
374
375
(defconst isar-keywords-proof-goal
376
'("have"
377
378
379
"thus"))
380
381
(defconst isar-keywords-proof-block
382
'("next"
383
"proof"))
384
385
(defconst isar-keywords-proof-open
386
'("{"))
387
388
(defconst isar-keywords-proof-close
389
'("}"))
390
391
(defconst isar-keywords-proof-chain
392
'("finally"
393
394
395
396
"with"))
397
398
(defconst isar-keywords-proof-decl
399
'("also"
400
401
402
403
404
405
406
"using"))
407
408
(defconst isar-keywords-proof-asm
409
'("assume"
410
411
412
413
"presume"))
414
415
(defconst isar-keywords-proof-asm-goal
416
'("obtain"))
417
418
(defconst isar-keywords-proof-script
419
'("apply"
420
421
422
423
"prefer"))
424
425
(provide 'isar-keywords)