equal
deleted
inserted
replaced
33 "cannot_undo" |
33 "cannot_undo" |
34 "case" |
34 "case" |
35 "cd" |
35 "cd" |
36 "chapter" |
36 "chapter" |
37 "class" |
37 "class" |
38 "class_instance" |
|
39 "classes" |
38 "classes" |
40 "classrel" |
39 "classrel" |
41 "clear_undos" |
40 "clear_undos" |
42 "codatatype" |
41 "codatatype" |
43 "code_alias" |
42 "code_alias" |
44 "code_class" |
|
45 "code_generate" |
43 "code_generate" |
46 "code_library" |
44 "code_library" |
47 "code_module" |
45 "code_module" |
48 "code_primclass" |
46 "code_primclass" |
49 "code_primconst" |
47 "code_primconst" |
214 "defines" |
212 "defines" |
215 "depending_on" |
213 "depending_on" |
216 "domains" |
214 "domains" |
217 "elimination" |
215 "elimination" |
218 "file" |
216 "file" |
219 "files" |
|
220 "fixes" |
217 "fixes" |
221 "imports" |
218 "imports" |
222 "in" |
219 "in" |
223 "includes" |
220 "includes" |
224 "induction" |
221 "induction" |
227 "infixr" |
224 "infixr" |
228 "intros" |
225 "intros" |
229 "is" |
226 "is" |
230 "monos" |
227 "monos" |
231 "notes" |
228 "notes" |
|
229 "obtains" |
232 "open" |
230 "open" |
233 "output" |
231 "output" |
234 "overloaded" |
232 "overloaded" |
235 "recursor_eqns" |
233 "recursor_eqns" |
236 "shows" |
234 "shows" |
340 "class" |
338 "class" |
341 "classes" |
339 "classes" |
342 "classrel" |
340 "classrel" |
343 "codatatype" |
341 "codatatype" |
344 "code_alias" |
342 "code_alias" |
345 "code_class" |
|
346 "code_generate" |
343 "code_generate" |
347 "code_library" |
344 "code_library" |
348 "code_module" |
345 "code_module" |
349 "code_primclass" |
346 "code_primclass" |
350 "code_primconst" |
347 "code_primconst" |
398 (defconst isar-keywords-theory-script |
395 (defconst isar-keywords-theory-script |
399 '("declare" |
396 '("declare" |
400 "inductive_cases")) |
397 "inductive_cases")) |
401 |
398 |
402 (defconst isar-keywords-theory-goal |
399 (defconst isar-keywords-theory-goal |
403 '("class_instance" |
400 '("corollary" |
404 "corollary" |
|
405 "instance" |
401 "instance" |
406 "interpretation" |
402 "interpretation" |
407 "lemma" |
403 "lemma" |
408 "theorem")) |
404 "theorem")) |
409 |
405 |