1.1 --- a/etc/isar-keywords-ZF.el	Sun Dec 14 15:50:21 2008 +0100
     1.2 +++ b/etc/isar-keywords-ZF.el	Sun Dec 14 18:45:16 2008 +0100
     1.3 @@ -40,9 +40,6 @@
     1.4      "chapter"
     1.5      "class"
     1.6      "class_deps"
     1.7 -    "class_interpret"
     1.8 -    "class_interpretation"
     1.9 -    "class_locale"
    1.10      "classes"
    1.11      "classrel"
    1.12      "codatatype"
    1.13 @@ -352,7 +349,6 @@
    1.14      "axiomatization"
    1.15      "axioms"
    1.16      "class"
    1.17 -    "class_locale"
    1.18      "classes"
    1.19      "classrel"
    1.20      "codatatype"
    1.21 @@ -415,8 +411,7 @@
    1.22    '("inductive_cases"))
    1.23  
    1.24  (defconst isar-keywords-theory-goal
    1.25 -  '("class_interpretation"
    1.26 -    "corollary"
    1.27 +  '("corollary"
    1.28      "instance"
    1.29      "interpretation"
    1.30      "lemma"
    1.31 @@ -443,8 +438,7 @@
    1.32      "subsubsect"))
    1.33  
    1.34  (defconst isar-keywords-proof-goal
    1.35 -  '("class_interpret"
    1.36 -    "have"
    1.37 +  '("have"
    1.38      "hence"
    1.39      "interpret"
    1.40      "invoke"))

     2.1 --- a/etc/isar-keywords.el	Sun Dec 14 15:50:21 2008 +0100
     2.2 +++ b/etc/isar-keywords.el	Sun Dec 14 18:45:16 2008 +0100
     2.3 @@ -45,6 +45,9 @@
     2.4      "chapter"
     2.5      "class"
     2.6      "class_deps"
     2.7 +    "class_interpret"
     2.8 +    "class_interpretation"
     2.9 +    "class_locale"
    2.10      "classes"
    2.11      "classrel"
    2.12      "code_abort"
    2.13 @@ -418,6 +421,7 @@
    2.14      "axiomatization"
    2.15      "axioms"
    2.16      "class"
    2.17 +    "class_locale"
    2.18      "classes"
    2.19      "classrel"
    2.20      "code_abort"
    2.21 @@ -501,6 +505,7 @@
    2.22  
    2.23  (defconst isar-keywords-theory-goal
    2.24    '("ax_specification"
    2.25 +    "class_interpretation"
    2.26      "corollary"
    2.27      "cpodef"
    2.28      "function"
    2.29 @@ -539,7 +544,8 @@
    2.30      "subsubsect"))
    2.31  
    2.32  (defconst isar-keywords-proof-goal
    2.33 -  '("have"
    2.34 +  '("class_interpret"
    2.35 +    "have"
    2.36      "hence"
    2.37      "interpret"
    2.38      "invoke"))