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