# HG changeset patch
# User ballarin
# Date 1225970991 -3600
# Node ID 21170e10c7456fd7e16dae7171b3e888e726ec99
# Parent  a08c37b478b2d17fab15cbce8a50bc7049b6ac53
Keyword 'includes' gone.

diff -r a08c37b478b2 -r 21170e10c745 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Thu Nov 06 11:52:50 2008 +0100
+++ b/etc/isar-keywords-ZF.el	Thu Nov 06 12:29:51 2008 +0100
@@ -226,7 +226,6 @@
     "if"
     "imports"
     "in"
-    "includes"
     "induction"
     "infix"
     "infixl"
diff -r a08c37b478b2 -r 21170e10c745 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Thu Nov 06 11:52:50 2008 +0100
+++ b/etc/isar-keywords.el	Thu Nov 06 12:29:51 2008 +0100
@@ -271,7 +271,6 @@
     "if"
     "imports"
     "in"
-    "includes"
     "infix"
     "infixl"
     "infixr"
diff -r a08c37b478b2 -r 21170e10c745 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Nov 06 11:52:50 2008 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Nov 06 12:29:51 2008 +0100
@@ -22,7 +22,7 @@
   "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
   "advanced", "and", "assumes", "attach", "begin", "binder",
   "constrains", "defines", "fixes", "for", "identifier", "if",
-  "imports", "in", "includes", "infix", "infixl", "infixr", "is",
+  "imports", "in", "infix", "infixl", "infixr", "is",
   "notes", "obtains", "open", "output", "overloaded", "shows",
   "structure", "unchecked", "uses", "where", "|"];