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