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