1
;;
2
;; Keyword classification tables for Isabelle/Isar.
3
;; This file was generated by Isabelle/HOLCF/IOA -- 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
"automaton"
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
"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
"defer_recdef"
51
"defs"
52
"disable_pr"
53
"domain"
54
"done"
55
"enable_pr"
56
"end"
57
"exit"
58
"finally"
59
"fix"
60
"from"
61
"full_prf"
62
"generate_code"
63
"global"
64
"have"
65
"header"
66
"hence"
67
"hide"
68
"inductive"
69
"inductive_cases"
70
"init_toplevel"
71
"instance"
72
"judgment"
73
"kill"
74
"kill_thy"
75
"lemma"
76
"lemmas"
77
"let"
78
"local"
79
"locale"
80
"method_setup"
81
"moreover"
82
"next"
83
"nonterminals"
84
"note"
85
"obtain"
86
"oops"
87
"oracle"
88
"parse_ast_translation"
89
"parse_translation"
90
"pr"
91
"prefer"
92
"presume"
93
"pretty_setmargin"
94
"prf"
95
"primrec"
96
"print_antiquotations"
97
"print_ast_translation"
98
"print_attributes"
99
"print_binds"
100
"print_cases"
101
"print_claset"
102
"print_commands"
103
"print_context"
104
"print_facts"
105
"print_induct_rules"
106
"print_locale"
107
"print_locales"
108
"print_methods"
109
"print_simpset"
110
"print_syntax"
111
"print_theorems"
112
"print_theory"
113
"print_trans_rules"
114
"print_translation"
115
"proof"
116
"prop"
117
"pwd"
118
"qed"
119
"quit"
120
"recdef"
121
"recdef_tc"
122
"record"
123
"redo"
124
"remove_thy"
125
"rep_datatype"
126
"sect"
127
"section"
128
"setup"
129
"show"
130
"sorry"
131
"subsect"
132
"subsection"
133
"subsubsect"
134
"subsubsection"
135
"syntax"
136
"term"
137
"text"
138
"text_raw"
139
"then"
140
"theorem"
141
"theorems"
142
"theory"
143
"thm"
144
"thm_deps"
145
"thms_containing"
146
"thus"
147
"token_translation"
148
"touch_all_thys"
149
"touch_child_thys"
150
"touch_thy"
151
"translations"
152
"txt"
153
"txt_raw"
154
"typ"
155
"typed_print_translation"
156
"typedecl"
157
"typedef"
158
"types"
159
"types_code"
160
"ultimately"
161
"undo"
162
"undos_proof"
163
"update_thy"
164
"update_thy_only"
165
"use"
166
"use_thy"
167
"use_thy_only"
168
"welcome"
169
"with"
170
"{"
171
"}"))
172
173
(defconst isar-keywords-minor
174
'("actions"
175
"and"
176
"assumes"
177
"binder"
178
"compose"
179
"concl"
180
"congs"
181
"defines"
182
"distinct"
183
"files"
184
"fixes"
185
"hide_action"
186
"hints"
187
"in"
188
"induction"
189
"infix"
190
"infixl"
191
"infixr"
192
"initially"
193
"inject"
194
"inputs"
195
"internals"
196
"intros"
197
"is"
198
"lazy"
199
"monos"
200
"morphisms"
201
"notes"
202
"output"
203
"outputs"
204
"overloaded"
205
"permissive"
206
"post"
207
"pre"
208
"rename"
209
"restrict"
210
"signature"
211
"states"
212
"structure"
213
"to"
214
"transitions"
215
"transrel"
216
"uses"
217
"using"
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
"undos_proof"))
237
238
(defconst isar-keywords-diag
239
'("ML"
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
"welcome"))
285
286
(defconst isar-keywords-theory-begin
287
'("theory"))
288
289
(defconst isar-keywords-theory-switch
290
'("context"))
291
292
(defconst isar-keywords-theory-end
293
'("end"))
294
295
(defconst isar-keywords-theory-heading
296
'("chapter"
297
298
299
"subsubsection"))
300
301
(defconst isar-keywords-theory-decl
302
'("ML_setup"
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
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
"types_code"))
348
349
(defconst isar-keywords-theory-script
350
'("declare"
351
"inductive_cases"))
352
353
(defconst isar-keywords-theory-goal
354
'("corollary"
355
356
357
358
359
"typedef"))
360
361
(defconst isar-keywords-qed
362
363
364
365
366
"sorry"))
367
368
(defconst isar-keywords-qed-block
369
'("qed"))
370
371
(defconst isar-keywords-qed-global
372
'("oops"))
373
374
(defconst isar-keywords-proof-heading
375
'("sect"
376
377
"subsubsect"))
378
379
(defconst isar-keywords-proof-goal
380
'("have"
381
382
383
"thus"))
384
385
(defconst isar-keywords-proof-block
386
'("next"
387
"proof"))
388
389
(defconst isar-keywords-proof-open
390
'("{"))
391
392
(defconst isar-keywords-proof-close
393
'("}"))
394
395
(defconst isar-keywords-proof-chain
396
'("finally"
397
398
399
400
"with"))
401
402
(defconst isar-keywords-proof-decl
403
'("also"
404
405
406
407
408
"txt_raw"))
409
410
(defconst isar-keywords-proof-asm
411
'("assume"
412
413
414
415
"presume"))
416
417
(defconst isar-keywords-proof-asm-goal
418
'("obtain"))
419
420
(defconst isar-keywords-proof-script
421
'("apply"
422
423
424
425
"prefer"))
426
427
(provide 'isar-keywords)