# HG changeset patch
# User wenzelm
# Date 1232576717 -3600
# Node ID 2db3537c35359b6de460d4a3de1ed90766a986a0
# Parent  fedb8be05f2401f62721a7ecc92d683efc1d078a
updated generated files;

diff -r fedb8be05f24 -r 2db3537c3535 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Wed Jan 21 23:21:44 2009 +0100
+++ b/etc/isar-keywords-ZF.el	Wed Jan 21 23:25:17 2009 +0100
@@ -3,14 +3,16 @@
 ;; Generated from Pure + Pure-ProofGeneral + FOL + ZF.
 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
 ;;
-;; $Id$
-;;
 
 (defconst isar-keywords-major
   '("\\."
     "\\.\\."
     "Isabelle\\.command"
+    "Isar\\.begin_document"
     "Isar\\.command"
+    "Isar\\.define_command"
+    "Isar\\.edit_document"
+    "Isar\\.end_document"
     "Isar\\.insert"
     "Isar\\.remove"
     "ML"
@@ -89,7 +91,6 @@
     "instantiation"
     "interpret"
     "interpretation"
-    "invoke"
     "judgment"
     "kill"
     "kill_thy"
@@ -135,7 +136,6 @@
     "print_drafts"
     "print_facts"
     "print_induct_rules"
-    "print_interps"
     "print_locale"
     "print_locales"
     "print_methods"
@@ -249,7 +249,11 @@
 
 (defconst isar-keywords-control
   '("Isabelle\\.command"
+    "Isar\\.begin_document"
     "Isar\\.command"
+    "Isar\\.define_command"
+    "Isar\\.edit_document"
+    "Isar\\.end_document"
     "Isar\\.insert"
     "Isar\\.remove"
     "ProofGeneral\\.inform_file_processed"
@@ -298,7 +302,6 @@
     "print_drafts"
     "print_facts"
     "print_induct_rules"
-    "print_interps"
     "print_locale"
     "print_locales"
     "print_methods"
@@ -438,8 +441,7 @@
 (defconst isar-keywords-proof-goal
   '("have"
     "hence"
-    "interpret"
-    "invoke"))
+    "interpret"))
 
 (defconst isar-keywords-proof-block
   '("next"
diff -r fedb8be05f24 -r 2db3537c3535 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Wed Jan 21 23:21:44 2009 +0100
+++ b/etc/isar-keywords.el	Wed Jan 21 23:25:17 2009 +0100
@@ -3,14 +3,16 @@
 ;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Nominal + HOL-Statespace.
 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
 ;;
-;; $Id$
-;;
 
 (defconst isar-keywords-major
   '("\\."
     "\\.\\."
     "Isabelle\\.command"
+    "Isar\\.begin_document"
     "Isar\\.command"
+    "Isar\\.define_command"
+    "Isar\\.edit_document"
+    "Isar\\.end_document"
     "Isar\\.insert"
     "Isar\\.remove"
     "ML"
@@ -46,9 +48,6 @@
     "chapter"
     "class"
     "class_deps"
-    "class_interpret"
-    "class_interpretation"
-    "class_locale"
     "classes"
     "classrel"
     "code_abort"
@@ -119,7 +118,6 @@
     "instantiation"
     "interpret"
     "interpretation"
-    "invoke"
     "judgment"
     "kill"
     "kill_thy"
@@ -172,7 +170,6 @@
     "print_drafts"
     "print_facts"
     "print_induct_rules"
-    "print_interps"
     "print_locale"
     "print_locales"
     "print_methods"
@@ -312,7 +309,11 @@
 
 (defconst isar-keywords-control
   '("Isabelle\\.command"
+    "Isar\\.begin_document"
     "Isar\\.command"
+    "Isar\\.define_command"
+    "Isar\\.edit_document"
+    "Isar\\.end_document"
     "Isar\\.insert"
     "Isar\\.remove"
     "ProofGeneral\\.inform_file_processed"
@@ -369,7 +370,6 @@
     "print_drafts"
     "print_facts"
     "print_induct_rules"
-    "print_interps"
     "print_locale"
     "print_locales"
     "print_methods"
@@ -423,7 +423,6 @@
     "axiomatization"
     "axioms"
     "class"
-    "class_locale"
     "classes"
     "classrel"
     "code_abort"
@@ -507,7 +506,6 @@
 
 (defconst isar-keywords-theory-goal
   '("ax_specification"
-    "class_interpretation"
     "corollary"
     "cpodef"
     "function"
@@ -546,11 +544,9 @@
     "subsubsect"))
 
 (defconst isar-keywords-proof-goal
-  '("class_interpret"
-    "have"
+  '("have"
     "hence"
-    "interpret"
-    "invoke"))
+    "interpret"))
 
 (defconst isar-keywords-proof-block
   '("next"
diff -r fedb8be05f24 -r 2db3537c3535 lib/jedit/isabelle.xml
--- a/lib/jedit/isabelle.xml	Wed Jan 21 23:21:44 2009 +0100
+++ b/lib/jedit/isabelle.xml	Wed Jan 21 23:25:17 2009 +0100
@@ -2,7 +2,6 @@
 <!DOCTYPE MODE SYSTEM "xmode.dtd">
 <!-- Generated from Pure + HOL + HOLCF + IOA + HOL-Nominal + HOL-Statespace + FOL + ZF. -->
 <!-- *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** -->
-<!-- $Id$ -->
 <MODE>
   <PROPS>
     <PROPERTY NAME="commentStart" VALUE="(*"/>
@@ -36,7 +35,11 @@
       <OPERATOR>.</OPERATOR>
       <OPERATOR>..</OPERATOR>
       <INVALID>Isabelle.command</INVALID>
+      <INVALID>Isar.begin_document</INVALID>
       <INVALID>Isar.command</INVALID>
+      <INVALID>Isar.define_command</INVALID>
+      <INVALID>Isar.edit_document</INVALID>
+      <INVALID>Isar.end_document</INVALID>
       <INVALID>Isar.insert</INVALID>
       <INVALID>Isar.remove</INVALID>
       <OPERATOR>ML</OPERATOR>
@@ -171,7 +174,6 @@
       <OPERATOR>interpret</OPERATOR>
       <OPERATOR>interpretation</OPERATOR>
       <KEYWORD4>intros</KEYWORD4>
-      <OPERATOR>invoke</OPERATOR>
       <KEYWORD4>is</KEYWORD4>
       <OPERATOR>judgment</OPERATOR>
       <INVALID>kill</INVALID>
@@ -239,7 +241,6 @@
       <LABEL>print_drafts</LABEL>
       <LABEL>print_facts</LABEL>
       <LABEL>print_induct_rules</LABEL>
-      <LABEL>print_interps</LABEL>
       <LABEL>print_locale</LABEL>
       <LABEL>print_locales</LABEL>
       <LABEL>print_methods</LABEL>