# HG changeset patch
# User wenzelm
# Date 1213458564 -7200
# Node ID 548e2d3105b9f0a6e31255cbe12e3580b3013842
# Parent  9a786d5f88213aa12105dce6523ff32c95efc335
updated generated file;

diff -r 9a786d5f8821 -r 548e2d3105b9 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Sat Jun 14 17:26:15 2008 +0200
+++ b/etc/isar-keywords-ZF.el	Sat Jun 14 17:49:24 2008 +0200
@@ -178,7 +178,6 @@
     "thm_deps"
     "thus"
     "thy_deps"
-    "token_translation"
     "touch_child_thys"
     "touch_thy"
     "translations"
@@ -396,7 +395,6 @@
     "text"
     "text_raw"
     "theorems"
-    "token_translation"
     "translations"
     "typed_print_translation"
     "typedecl"
diff -r 9a786d5f8821 -r 548e2d3105b9 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Sat Jun 14 17:26:15 2008 +0200
+++ b/etc/isar-keywords.el	Sat Jun 14 17:49:24 2008 +0200
@@ -52,7 +52,6 @@
     "code_module"
     "code_modulename"
     "code_monad"
-    "code_props"
     "code_reserved"
     "code_thms"
     "code_type"
@@ -217,7 +216,6 @@
     "thm_deps"
     "thus"
     "thy_deps"
-    "token_translation"
     "touch_child_thys"
     "touch_thy"
     "translations"
@@ -420,7 +418,6 @@
     "code_module"
     "code_modulename"
     "code_monad"
-    "code_props"
     "code_reserved"
     "code_type"
     "coinductive"
@@ -480,7 +477,6 @@
     "text"
     "text_raw"
     "theorems"
-    "token_translation"
     "translations"
     "typed_print_translation"
     "typedecl"
diff -r 9a786d5f8821 -r 548e2d3105b9 lib/jedit/isabelle.xml
--- a/lib/jedit/isabelle.xml	Sat Jun 14 17:26:15 2008 +0200
+++ b/lib/jedit/isabelle.xml	Sat Jun 14 17:49:24 2008 +0200
@@ -82,7 +82,6 @@
       <OPERATOR>code_module</OPERATOR>
       <OPERATOR>code_modulename</OPERATOR>
       <OPERATOR>code_monad</OPERATOR>
-      <OPERATOR>code_props</OPERATOR>
       <OPERATOR>code_reserved</OPERATOR>
       <LABEL>code_thms</LABEL>
       <OPERATOR>code_type</OPERATOR>
@@ -297,7 +296,6 @@
       <KEYWORD2>thus</KEYWORD2>
       <LABEL>thy_deps</LABEL>
       <KEYWORD4>to</KEYWORD4>
-      <OPERATOR>token_translation</OPERATOR>
       <LABEL>touch_child_thys</LABEL>
       <LABEL>touch_thy</LABEL>
       <KEYWORD4>transitions</KEYWORD4>