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
"induction"
184
"infix"
185
"infixl"
186
"infixr"
187
"intros"
188
"is"
189
"monos"
190
"notes"
191
"output"
192
"overloaded"
193
"recursor_eqns"
194
"structure"
195
"type_elims"
196
"type_intros"
197
"uses"
198
"where"))
199
200
(defconst isar-keywords-control
201
'("ProofGeneral\\.context_thy_only"
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
"undos_proof"))
217
218
(defconst isar-keywords-diag
219
'("ML"
220
221
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
"welcome"))
267
268
(defconst isar-keywords-theory-begin
269
'("theory"))
270
271
(defconst isar-keywords-theory-switch
272
'("context"))
273
274
(defconst isar-keywords-theory-end
275
'("end"))
276
277
(defconst isar-keywords-theory-heading
278
'("chapter"
279
280
281
"subsubsection"))
282
283
(defconst isar-keywords-theory-decl
284
'("ML_setup"
285
286
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
"types_code"))
326
327
(defconst isar-keywords-theory-script
328
'("declare"
329
"inductive_cases"))
330
331
(defconst isar-keywords-theory-goal
332
'("corollary"
333
334
335
"theorem"))
336
337
(defconst isar-keywords-qed
338
339
340
341
342
"sorry"))
343
344
(defconst isar-keywords-qed-block
345
'("qed"))
346
347
(defconst isar-keywords-qed-global
348
'("oops"))
349
350
(defconst isar-keywords-proof-heading
351
'("sect"
352
353
"subsubsect"))
354
355
(defconst isar-keywords-proof-goal
356
'("have"
357
358
359
"thus"))
360
361
(defconst isar-keywords-proof-block
362
'("next"
363
"proof"))
364
365
(defconst isar-keywords-proof-open
366
'("{"))
367
368
(defconst isar-keywords-proof-close
369
'("}"))
370
371
(defconst isar-keywords-proof-chain
372
'("finally"
373
374
375
376
"with"))
377
378
(defconst isar-keywords-proof-decl
379
'("also"
380
381
382
383
384
385
"using"))
386
387
(defconst isar-keywords-proof-asm
388
'("assume"
389
390
391
392
"presume"))
393
394
(defconst isar-keywords-proof-asm-goal
395
'("obtain"))
396
397
(defconst isar-keywords-proof-script
398
'("apply"
399
400
401
402
"prefer"))
403
404
(provide 'isar-keywords)