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\\.process_pgip"
19
"ProofGeneral\\.redo"
20
"ProofGeneral\\.restart"
21
"ProofGeneral\\.try_context_thy_only"
22
"ProofGeneral\\.undo"
23
"also"
24
"apply"
25
"apply_end"
26
"arities"
27
"assume"
28
"axclass"
29
"axioms"
30
"back"
31
"by"
32
"cannot_undo"
33
"case"
34
"cd"
35
"chapter"
36
"classes"
37
"classrel"
38
"clear_undos"
39
"codatatype"
40
"coinductive"
41
"commit"
42
"constdefs"
43
"consts"
44
"consts_code"
45
"context"
46
"corollary"
47
"datatype"
48
"declare"
49
"def"
50
"defaultsort"
51
"defer"
52
"defs"
53
"disable_pr"
54
"display_drafts"
55
"done"
56
"enable_pr"
57
"end"
58
"exit"
59
"extract"
60
"extract_type"
61
"finalconsts"
62
"finally"
63
"find_rewrites"
64
"fix"
65
"from"
66
"full_prf"
67
"generate_code"
68
"global"
69
"have"
70
"header"
71
"hence"
72
"hide"
73
"inductive"
74
"inductive_cases"
75
"init_toplevel"
76
"instance"
77
"instantiate"
78
"interpret"
79
"interpretation"
80
"judgment"
81
"kill"
82
"kill_thy"
83
"lemma"
84
"lemmas"
85
"let"
86
"local"
87
"locale"
88
"method_setup"
89
"moreover"
90
"next"
91
"no_syntax"
92
"nonterminals"
93
"note"
94
"obtain"
95
"oops"
96
"oracle"
97
"parse_ast_translation"
98
"parse_translation"
99
"pr"
100
"prefer"
101
"presume"
102
"pretty_setmargin"
103
"prf"
104
"primrec"
105
"print_antiquotations"
106
"print_ast_translation"
107
"print_attributes"
108
"print_binds"
109
"print_cases"
110
"print_claset"
111
"print_commands"
112
"print_context"
113
"print_drafts"
114
"print_facts"
115
"print_induct_rules"
116
"print_interps"
117
"print_intros"
118
"print_locale"
119
"print_locales"
120
"print_methods"
121
"print_rules"
122
"print_simpset"
123
"print_syntax"
124
"print_tcset"
125
"print_theorems"
126
"print_theory"
127
"print_trans_rules"
128
"print_translation"
129
"proof"
130
"prop"
131
"pwd"
132
"qed"
133
"quickcheck"
134
"quickcheck_params"
135
"quit"
136
"realizability"
137
"realizers"
138
"redo"
139
"remove_thy"
140
"rep_datatype"
141
"sect"
142
"section"
143
"setup"
144
"show"
145
"sorry"
146
"subsect"
147
"subsection"
148
"subsubsect"
149
"subsubsection"
150
"syntax"
151
"term"
152
"text"
153
"text_raw"
154
"then"
155
"theorem"
156
"theorems"
157
"theory"
158
"thm"
159
"thm_deps"
160
"thms_containing"
161
"thus"
162
"token_translation"
163
"touch_all_thys"
164
"touch_child_thys"
165
"touch_thy"
166
"translations"
167
"txt"
168
"txt_raw"
169
"typ"
170
"typed_print_translation"
171
"typedecl"
172
"types"
173
"types_code"
174
"ultimately"
175
"undo"
176
"undos_proof"
177
"update_thy"
178
"update_thy_only"
179
"use"
180
"use_thy"
181
"use_thy_only"
182
"using"
183
"welcome"
184
"with"
185
"{"
186
"}"))
187
188
(defconst isar-keywords-minor
189
'("advanced"
190
"and"
191
"assumes"
192
"begin"
193
"binder"
194
"case_eqns"
195
"con_defs"
196
"concl"
197
"defines"
198
"domains"
199
"elimination"
200
"files"
201
"fixes"
202
"imports"
203
"in"
204
"includes"
205
"induction"
206
"infix"
207
"infixl"
208
"infixr"
209
"intros"
210
"is"
211
"monos"
212
"notes"
213
"open"
214
"output"
215
"overloaded"
216
"recursor_eqns"
217
"shows"
218
"structure"
219
"type_elims"
220
"type_intros"
221
"where"))
222
223
(defconst isar-keywords-control
224
'("ProofGeneral\\.context_thy_only"
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
"undos_proof"))
242
243
(defconst isar-keywords-diag
244
'("ML"
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
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
"welcome"))
298
299
(defconst isar-keywords-theory-begin
300
'("theory"))
301
302
(defconst isar-keywords-theory-switch
303
'("context"))
304
305
(defconst isar-keywords-theory-end
306
'("end"))
307
308
(defconst isar-keywords-theory-heading
309
'("chapter"
310
311
312
"subsubsection"))
313
314
(defconst isar-keywords-theory-decl
315
'("ML_setup"
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
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
"types_code"))
364
365
(defconst isar-keywords-theory-script
366
'("declare"
367
"inductive_cases"))
368
369
(defconst isar-keywords-theory-goal
370
'("corollary"
371
372
373
374
"theorem"))
375
376
(defconst isar-keywords-qed
377
378
379
380
381
"sorry"))
382
383
(defconst isar-keywords-qed-block
384
'("qed"))
385
386
(defconst isar-keywords-qed-global
387
'("oops"))
388
389
(defconst isar-keywords-proof-heading
390
'("sect"
391
392
"subsubsect"))
393
394
(defconst isar-keywords-proof-goal
395
'("have"
396
397
398
399
"thus"))
400
401
(defconst isar-keywords-proof-block
402
'("next"
403
"proof"))
404
405
(defconst isar-keywords-proof-open
406
'("{"))
407
408
(defconst isar-keywords-proof-close
409
'("}"))
410
411
(defconst isar-keywords-proof-chain
412
'("finally"
413
414
415
416
"with"))
417
418
(defconst isar-keywords-proof-decl
419
'("also"
420
421
422
423
424
425
426
"using"))
427
428
(defconst isar-keywords-proof-asm
429
'("assume"
430
431
432
433
"presume"))
434
435
(defconst isar-keywords-proof-asm-goal
436
'("obtain"))
437
438
(defconst isar-keywords-proof-script
439
'("apply"
440
441
442
443
"prefer"))
444
445
(provide 'isar-keywords)