1.1 --- a/etc/isar-keywords-ZF.el	Sun Dec 02 20:38:42 2007 +0100
     1.2 +++ b/etc/isar-keywords-ZF.el	Mon Dec 03 16:04:13 2007 +0100
     1.3 @@ -81,7 +81,6 @@
     1.4      "inductive_cases"
     1.5      "init_toplevel"
     1.6      "instance"
     1.7 -    "instance_proof"
     1.8      "instantiation"
     1.9      "interpret"
    1.10      "interpretation"
    1.11 @@ -106,6 +105,7 @@
    1.12      "obtain"
    1.13      "oops"
    1.14      "oracle"
    1.15 +    "overloading"
    1.16      "parse_ast_translation"
    1.17      "parse_translation"
    1.18      "pr"
    1.19 @@ -378,6 +378,7 @@
    1.20      "nonterminals"
    1.21      "notation"
    1.22      "oracle"
    1.23 +    "overloading"
    1.24      "parse_ast_translation"
    1.25      "parse_translation"
    1.26      "primrec"
    1.27 @@ -406,7 +407,6 @@
    1.28  (defconst isar-keywords-theory-goal
    1.29    '("corollary"
    1.30      "instance"
    1.31 -    "instance_proof"
    1.32      "interpretation"
    1.33      "lemma"
    1.34      "subclass"

     2.1 --- a/etc/isar-keywords.el	Sun Dec 02 20:38:42 2007 +0100
     2.2 +++ b/etc/isar-keywords.el	Mon Dec 03 16:04:13 2007 +0100
     2.3 @@ -106,7 +106,6 @@
     2.4      "inductive_set"
     2.5      "init_toplevel"
     2.6      "instance"
     2.7 -    "instance_proof"
     2.8      "instantiation"
     2.9      "interpret"
    2.10      "interpretation"
    2.11 @@ -135,6 +134,7 @@
    2.12      "obtain"
    2.13      "oops"
    2.14      "oracle"
    2.15 +    "overloading"
    2.16      "parse_ast_translation"
    2.17      "parse_translation"
    2.18      "pcpodef"
    2.19 @@ -466,6 +466,7 @@
    2.20      "nonterminals"
    2.21      "notation"
    2.22      "oracle"
    2.23 +    "overloading"
    2.24      "parse_ast_translation"
    2.25      "parse_translation"
    2.26      "primrec"
    2.27 @@ -501,7 +502,6 @@
    2.28      "cpodef"
    2.29      "function"
    2.30      "instance"
    2.31 -    "instance_proof"
    2.32      "interpretation"
    2.33      "lemma"
    2.34      "nominal_inductive"

     3.1 --- a/lib/jedit/isabelle.xml	Sun Dec 02 20:38:42 2007 +0100
     3.2 +++ b/lib/jedit/isabelle.xml	Mon Dec 03 16:04:13 2007 +0100
     3.3 @@ -163,7 +163,6 @@
     3.4        <KEYWORD4>inject</KEYWORD4>
     3.5        <KEYWORD4>inputs</KEYWORD4>
     3.6        <OPERATOR>instance</OPERATOR>
     3.7 -      <OPERATOR>instance_proof</OPERATOR>
     3.8        <OPERATOR>instantiation</OPERATOR>
     3.9        <KEYWORD4>internals</KEYWORD4>
    3.10        <OPERATOR>interpret</OPERATOR>
    3.11 @@ -206,6 +205,7 @@
    3.12        <KEYWORD4>output</KEYWORD4>
    3.13        <KEYWORD4>outputs</KEYWORD4>
    3.14        <KEYWORD4>overloaded</KEYWORD4>
    3.15 +      <OPERATOR>overloading</OPERATOR>
    3.16        <OPERATOR>parse_ast_translation</OPERATOR>
    3.17        <OPERATOR>parse_translation</OPERATOR>
    3.18        <OPERATOR>pcpodef</OPERATOR>