equal
deleted
inserted
replaced
38 "case" |
38 "case" |
39 "cd" |
39 "cd" |
40 "chapter" |
40 "chapter" |
41 "class" |
41 "class" |
42 "class_deps" |
42 "class_deps" |
43 "class_interpret" |
|
44 "class_interpretation" |
|
45 "class_locale" |
|
46 "classes" |
43 "classes" |
47 "classrel" |
44 "classrel" |
48 "codatatype" |
45 "codatatype" |
49 "code_datatype" |
46 "code_datatype" |
50 "code_library" |
47 "code_library" |
350 "arities" |
347 "arities" |
351 "axclass" |
348 "axclass" |
352 "axiomatization" |
349 "axiomatization" |
353 "axioms" |
350 "axioms" |
354 "class" |
351 "class" |
355 "class_locale" |
|
356 "classes" |
352 "classes" |
357 "classrel" |
353 "classrel" |
358 "codatatype" |
354 "codatatype" |
359 "code_datatype" |
355 "code_datatype" |
360 "code_library" |
356 "code_library" |
413 |
409 |
414 (defconst isar-keywords-theory-script |
410 (defconst isar-keywords-theory-script |
415 '("inductive_cases")) |
411 '("inductive_cases")) |
416 |
412 |
417 (defconst isar-keywords-theory-goal |
413 (defconst isar-keywords-theory-goal |
418 '("class_interpretation" |
414 '("corollary" |
419 "corollary" |
|
420 "instance" |
415 "instance" |
421 "interpretation" |
416 "interpretation" |
422 "lemma" |
417 "lemma" |
423 "subclass" |
418 "subclass" |
424 "sublocale" |
419 "sublocale" |
441 '("sect" |
436 '("sect" |
442 "subsect" |
437 "subsect" |
443 "subsubsect")) |
438 "subsubsect")) |
444 |
439 |
445 (defconst isar-keywords-proof-goal |
440 (defconst isar-keywords-proof-goal |
446 '("class_interpret" |
441 '("have" |
447 "have" |
|
448 "hence" |
442 "hence" |
449 "interpret" |
443 "interpret" |
450 "invoke")) |
444 "invoke")) |
451 |
445 |
452 (defconst isar-keywords-proof-block |
446 (defconst isar-keywords-proof-block |