Keyword 'includes' gone.
authorballarin
Thu, 06 Nov 2008 12:29:51 +0100
changeset 28721 21170e10c745
parent 28720 a08c37b478b2
child 28722 bdb694e18bf8
Keyword 'includes' gone.
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/Pure/Isar/isar_syn.ML
--- 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"
--- 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"
--- 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", "|"];