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