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_simpset"
108
"print_syntax"
109
"print_theorems"
110
"print_theory"
111
"print_trans_rules"
112
"print_translation"
113
"proof"
114
"prop"
115
"pwd"
116
"qed"
117
"quit"
118
"redo"
119
"remove_thy"
120
"sect"
121
"section"
122
"setup"
123
"show"
124
"sorry"
125
"subsect"
126
"subsection"
127
"subsubsect"
128
"subsubsection"
129
"syntax"
130
"term"
131
"text"
132
"text_raw"
133
"then"
134
"theorem"
135
"theorems"
136
"theory"
137
"thm"
138
"thm_deps"
139
"thms_containing"
140
"thus"
141
"token_translation"
142
"touch_all_thys"
143
"touch_child_thys"
144
"touch_thy"
145
"translations"
146
"txt"
147
"txt_raw"
148
"typ"
149
"typed_print_translation"
150
"typedecl"
151
"types"
152
"types_code"
153
"ultimately"
154
"undo"
155
"undos_proof"
156
"update_thy"
157
"update_thy_only"
158
"use"
159
"use_thy"
160
"use_thy_only"
161
"welcome"
162
"with"
163
"{"
164
"}"))
165
166
(defconst isar-keywords-minor
167
'("and"
168
"assumes"
169
"binder"
170
"con_defs"
171
"concl"
172
"defines"
173
"domains"
174
"files"
175
"fixes"
176
"in"
177
"infix"
178
"infixl"
179
"infixr"
180
"intros"
181
"is"
182
"monos"
183
"notes"
184
"output"
185
"overloaded"
186
"structure"
187
"type_elims"
188
"type_intros"
189
"uses"
190
"where"))
191
192
(defconst isar-keywords-control
193
'("ProofGeneral\\.context_thy_only"
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
"undos_proof"))
209
210
(defconst isar-keywords-diag
211
'("ML"
212
213
214
215
216
217
218
219
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
"welcome"))
257
258
(defconst isar-keywords-theory-begin
259
'("theory"))
260
261
(defconst isar-keywords-theory-switch
262
'("context"))
263
264
(defconst isar-keywords-theory-end
265
'("end"))
266
267
(defconst isar-keywords-theory-heading
268
'("chapter"
269
270
271
"subsubsection"))
272
273
(defconst isar-keywords-theory-decl
274
'("ML_setup"
275
276
277
278
279
280
281
282
283
284
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
"types_code"))
315
316
(defconst isar-keywords-theory-script
317
'("declare"
318
"inductive_cases"))
319
320
(defconst isar-keywords-theory-goal
321
'("corollary"
322
323
324
"theorem"))
325
326
(defconst isar-keywords-qed
327
328
329
330
331
"sorry"))
332
333
(defconst isar-keywords-qed-block
334
'("qed"))
335
336
(defconst isar-keywords-qed-global
337
'("oops"))
338
339
(defconst isar-keywords-proof-heading
340
'("sect"
341
342
"subsubsect"))
343
344
(defconst isar-keywords-proof-goal
345
'("have"
346
347
348
"thus"))
349
350
(defconst isar-keywords-proof-block
351
'("next"
352
"proof"))
353
354
(defconst isar-keywords-proof-open
355
'("{"))
356
357
(defconst isar-keywords-proof-close
358
'("}"))
359
360
(defconst isar-keywords-proof-chain
361
'("finally"
362
363
364
365
"with"))
366
367
(defconst isar-keywords-proof-decl
368
'("also"
369
370
371
372
373
"txt_raw"))
374
375
(defconst isar-keywords-proof-asm
376
'("assume"
377
378
379
380
"presume"))
381
382
(defconst isar-keywords-proof-asm-goal
383
'("obtain"))
384
385
(defconst isar-keywords-proof-script
386
'("apply"
387
388
389
390
"prefer"))
391
392
(provide 'isar-keywords)