# HG changeset patch
# User haftmann
# Date 1213104601 -7200
# Node ID a98cd7450204b5dce9cff02c21b5ded39462e796
# Parent  864d29f11c9d8532e06c2c28aa56d658d3ff2dbf
updated

diff -r 864d29f11c9d -r a98cd7450204 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Tue Jun 10 14:32:58 2008 +0200
+++ b/etc/isar-keywords.el	Tue Jun 10 15:30:01 2008 +0200
@@ -41,11 +41,11 @@
     "class_deps"
     "classes"
     "classrel"
+    "code_abort"
     "code_class"
     "code_const"
     "code_datatype"
     "code_deps"
-    "code_exception"
     "code_include"
     "code_instance"
     "code_library"
@@ -257,7 +257,6 @@
     "constrains"
     "contains"
     "defines"
-    "distinct"
     "file"
     "fixes"
     "for"
@@ -268,12 +267,10 @@
     "imports"
     "in"
     "includes"
-    "induction"
     "infix"
     "infixl"
     "infixr"
     "initially"
-    "inject"
     "inputs"
     "internals"
     "is"
@@ -413,10 +410,10 @@
     "class"
     "classes"
     "classrel"
+    "code_abort"
     "code_class"
     "code_const"
     "code_datatype"
-    "code_exception"
     "code_include"
     "code_instance"
     "code_library"
@@ -476,7 +473,6 @@
     "recdef"
     "record"
     "refute_params"
-    "rep_datatype"
     "setup"
     "simproc_setup"
     "statespace"
@@ -507,6 +503,7 @@
     "nominal_primrec"
     "pcpodef"
     "recdef_tc"
+    "rep_datatype"
     "specification"
     "subclass"
     "termination"
diff -r 864d29f11c9d -r a98cd7450204 lib/jedit/isabelle.xml
--- a/lib/jedit/isabelle.xml	Tue Jun 10 14:32:58 2008 +0200
+++ b/lib/jedit/isabelle.xml	Tue Jun 10 15:30:01 2008 +0200
@@ -71,11 +71,11 @@
       <OPERATOR>classes</OPERATOR>
       <OPERATOR>classrel</OPERATOR>
       <OPERATOR>codatatype</OPERATOR>
+      <OPERATOR>code_abort</OPERATOR>
       <OPERATOR>code_class</OPERATOR>
       <OPERATOR>code_const</OPERATOR>
       <OPERATOR>code_datatype</OPERATOR>
       <LABEL>code_deps</LABEL>
-      <OPERATOR>code_exception</OPERATOR>
       <OPERATOR>code_include</OPERATOR>
       <OPERATOR>code_instance</OPERATOR>
       <OPERATOR>code_library</OPERATOR>
@@ -112,7 +112,6 @@
       <OPERATOR>defs</OPERATOR>
       <LABEL>disable_pr</LABEL>
       <LABEL>display_drafts</LABEL>
-      <KEYWORD4>distinct</KEYWORD4>
       <OPERATOR>domain</OPERATOR>
       <KEYWORD4>domains</KEYWORD4>
       <OPERATOR>done</OPERATOR>
@@ -160,7 +159,6 @@
       <KEYWORD4>infixr</KEYWORD4>
       <INVALID>init_toplevel</INVALID>
       <KEYWORD4>initially</KEYWORD4>
-      <KEYWORD4>inject</KEYWORD4>
       <KEYWORD4>inputs</KEYWORD4>
       <OPERATOR>instance</OPERATOR>
       <OPERATOR>instantiation</OPERATOR>