--- a/etc/isar-keywords-ZF.el Sun Dec 02 20:38:42 2007 +0100
+++ b/etc/isar-keywords-ZF.el Mon Dec 03 16:04:13 2007 +0100
@@ -81,7 +81,6 @@
"inductive_cases"
"init_toplevel"
"instance"
- "instance_proof"
"instantiation"
"interpret"
"interpretation"
@@ -106,6 +105,7 @@
"obtain"
"oops"
"oracle"
+ "overloading"
"parse_ast_translation"
"parse_translation"
"pr"
@@ -378,6 +378,7 @@
"nonterminals"
"notation"
"oracle"
+ "overloading"
"parse_ast_translation"
"parse_translation"
"primrec"
@@ -406,7 +407,6 @@
(defconst isar-keywords-theory-goal
'("corollary"
"instance"
- "instance_proof"
"interpretation"
"lemma"
"subclass"
--- a/etc/isar-keywords.el Sun Dec 02 20:38:42 2007 +0100
+++ b/etc/isar-keywords.el Mon Dec 03 16:04:13 2007 +0100
@@ -106,7 +106,6 @@
"inductive_set"
"init_toplevel"
"instance"
- "instance_proof"
"instantiation"
"interpret"
"interpretation"
@@ -135,6 +134,7 @@
"obtain"
"oops"
"oracle"
+ "overloading"
"parse_ast_translation"
"parse_translation"
"pcpodef"
@@ -466,6 +466,7 @@
"nonterminals"
"notation"
"oracle"
+ "overloading"
"parse_ast_translation"
"parse_translation"
"primrec"
@@ -501,7 +502,6 @@
"cpodef"
"function"
"instance"
- "instance_proof"
"interpretation"
"lemma"
"nominal_inductive"
--- a/lib/jedit/isabelle.xml Sun Dec 02 20:38:42 2007 +0100
+++ b/lib/jedit/isabelle.xml Mon Dec 03 16:04:13 2007 +0100
@@ -163,7 +163,6 @@
<KEYWORD4>inject</KEYWORD4>
<KEYWORD4>inputs</KEYWORD4>
<OPERATOR>instance</OPERATOR>
- <OPERATOR>instance_proof</OPERATOR>
<OPERATOR>instantiation</OPERATOR>
<KEYWORD4>internals</KEYWORD4>
<OPERATOR>interpret</OPERATOR>
@@ -206,6 +205,7 @@
<KEYWORD4>output</KEYWORD4>
<KEYWORD4>outputs</KEYWORD4>
<KEYWORD4>overloaded</KEYWORD4>
+ <OPERATOR>overloading</OPERATOR>
<OPERATOR>parse_ast_translation</OPERATOR>
<OPERATOR>parse_translation</OPERATOR>
<OPERATOR>pcpodef</OPERATOR>