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
"datatype"
45
"declare"
46
"def"
47
"defaultsort"
48
"defer"
49
"defer_recdef"
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
"method_setup"
78
"moreover"
79
"next"
80
"nonterminals"
81
"note"
82
"obtain"
83
"oops"
84
"oracle"
85
"parse_ast_translation"
86
"parse_translation"
87
"pr"
88
"prefer"
89
"presume"
90
"pretty_setmargin"
91
"prf"
92
"primrec"
93
"print_antiquotations"
94
"print_ast_translation"
95
"print_attributes"
96
"print_binds"
97
"print_cases"
98
"print_claset"
99
"print_commands"
100
"print_context"
101
"print_facts"
102
"print_methods"
103
"print_simpset"
104
"print_syntax"
105
"print_theorems"
106
"print_theory"
107
"print_trans_rules"
108
"print_translation"
109
"proof"
110
"prop"
111
"pwd"
112
"qed"
113
"quit"
114
"recdef"
115
"recdef_tc"
116
"record"
117
"redo"
118
"remove_thy"
119
"rep_datatype"
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
"typedef"
152
"types"
153
"types_code"
154
"ultimately"
155
"undo"
156
"undos_proof"
157
"update_thy"
158
"update_thy_only"
159
"use"
160
"use_thy"
161
"use_thy_only"
162
"welcome"
163
"with"
164
"{"
165
"}"))
166
167
(defconst isar-keywords-minor
168
'("actions"
169
"and"
170
"binder"
171
"compose"
172
"con_defs"
173
"concl"
174
"congs"
175
"distinct"
176
"files"
177
"hide_action"
178
"hints"
179
"in"
180
"induction"
181
"infixl"
182
"infixr"
183
"initially"
184
"inject"
185
"inputs"
186
"internals"
187
"intros"
188
"is"
189
"monos"
190
"output"
191
"outputs"
192
"overloaded"
193
"permissive"
194
"post"
195
"pre"
196
"rename"
197
"restrict"
198
"signature"
199
"states"
200
"to"
201
"transitions"
202
"transrel"
203
"using"
204
"where"))
205
206
(defconst isar-keywords-control
207
'("ProofGeneral\\.context_thy_only"
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
"undos_proof"))
223
224
(defconst isar-keywords-diag
225
'("ML"
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
"welcome"))
268
269
(defconst isar-keywords-theory-begin
270
'("theory"))
271
272
(defconst isar-keywords-theory-switch
273
'("context"))
274
275
(defconst isar-keywords-theory-end
276
'("end"))
277
278
(defconst isar-keywords-theory-heading
279
'("chapter"
280
281
282
"subsubsection"))
283
284
(defconst isar-keywords-theory-decl
285
'("ML_setup"
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
326
327
328
"types_code"))
329
330
(defconst isar-keywords-theory-script
331
'("declare"
332
"inductive_cases"))
333
334
(defconst isar-keywords-theory-goal
335
'("instance"
336
337
338
339
"typedef"))
340
341
(defconst isar-keywords-qed
342
343
344
345
346
"sorry"))
347
348
(defconst isar-keywords-qed-block
349
'("qed"))
350
351
(defconst isar-keywords-qed-global
352
'("oops"))
353
354
(defconst isar-keywords-proof-heading
355
'("sect"
356
357
"subsubsect"))
358
359
(defconst isar-keywords-proof-goal
360
'("have"
361
362
363
"thus"))
364
365
(defconst isar-keywords-proof-block
366
'("next"
367
"proof"))
368
369
(defconst isar-keywords-proof-open
370
'("{"))
371
372
(defconst isar-keywords-proof-close
373
'("}"))
374
375
(defconst isar-keywords-proof-chain
376
'("finally"
377
378
379
380
"with"))
381
382
(defconst isar-keywords-proof-decl
383
'("also"
384
385
386
387
388
"txt_raw"))
389
390
(defconst isar-keywords-proof-asm
391
'("assume"
392
393
394
395
"presume"))
396
397
(defconst isar-keywords-proof-asm-goal
398
'("obtain"))
399
400
(defconst isar-keywords-proof-script
401
'("apply"
402
403
404
405
"prefer"))
406
407
(provide 'isar-keywords)