# HG changeset patch
# User wenzelm
# Date 1185394854 -7200
# Node ID bf352c4c499bd8d30a704e968d8c9d9a36784400
# Parent  d4417ba26706e239a3444b32fb6866c5dfd18e89
updated;

diff -r d4417ba26706 -r bf352c4c499b etc/isar-keywords-HOL-Nominal.el
--- a/etc/isar-keywords-HOL-Nominal.el	Wed Jul 25 22:20:53 2007 +0200
+++ b/etc/isar-keywords-HOL-Nominal.el	Wed Jul 25 22:20:54 2007 +0200
@@ -220,10 +220,8 @@
     "undos_proof"
     "unfolding"
     "update_thy"
-    "update_thy_only"
     "use"
     "use_thy"
-    "use_thy_only"
     "using"
     "value"
     "welcome"
@@ -355,10 +353,8 @@
     "touch_thy"
     "typ"
     "update_thy"
-    "update_thy_only"
     "use"
     "use_thy"
-    "use_thy_only"
     "value"
     "welcome"))
 
diff -r d4417ba26706 -r bf352c4c499b etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Wed Jul 25 22:20:53 2007 +0200
+++ b/etc/isar-keywords-ZF.el	Wed Jul 25 22:20:54 2007 +0200
@@ -202,10 +202,8 @@
     "undos_proof"
     "unfolding"
     "update_thy"
-    "update_thy_only"
     "use"
     "use_thy"
-    "use_thy_only"
     "using"
     "value"
     "welcome"
@@ -333,10 +331,8 @@
     "touch_thy"
     "typ"
     "update_thy"
-    "update_thy_only"
     "use"
     "use_thy"
-    "use_thy_only"
     "value"
     "welcome"))
 
diff -r d4417ba26706 -r bf352c4c499b etc/isar-keywords.el
--- a/etc/isar-keywords.el	Wed Jul 25 22:20:53 2007 +0200
+++ b/etc/isar-keywords.el	Wed Jul 25 22:20:54 2007 +0200
@@ -153,6 +153,7 @@
     "print_locale"
     "print_locales"
     "print_methods"
+    "print_options"
     "print_rules"
     "print_simpset"
     "print_statement"
@@ -221,10 +222,8 @@
     "undos_proof"
     "unfolding"
     "update_thy"
-    "update_thy_only"
     "use"
     "use_thy"
-    "use_thy_only"
     "using"
     "value"
     "welcome"
@@ -347,6 +346,7 @@
     "print_locale"
     "print_locales"
     "print_methods"
+    "print_options"
     "print_rules"
     "print_simpset"
     "print_statement"
@@ -369,10 +369,8 @@
     "touch_thy"
     "typ"
     "update_thy"
-    "update_thy_only"
     "use"
     "use_thy"
-    "use_thy_only"
     "value"
     "welcome"))