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