From 36d34a997778a7b17311fb81ed0d18cd9a9324b9 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Wed, 16 Aug 2000 15:31:39 +0000
Subject: added isar-keywords-proof-improper; tuned;

---
 isar/isar-keywords.el | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/isar/isar-keywords.el b/isar/isar-keywords.el
index 14839e30..8e027618 100644
--- a/isar/isar-keywords.el
+++ b/isar/isar-keywords.el
@@ -40,6 +40,7 @@
     "consts"
     "context"
     "datatype"
+    "declare"
     "def"
     "defaultsort"
     "defer"
@@ -169,9 +170,10 @@
     "infixl"
     "infixr"
     "inject"
-    "intrs"
+    "intros"
     "is"
     "monos"
+    "of"
     "output"
     "overloaded"
     "where"))
@@ -269,7 +271,6 @@
     "global"
     "hide"
     "inductive"
-    "inductive_cases"
     "judgment"
     "lemmas"
     "local"
@@ -295,6 +296,10 @@
     "typedecl"
     "types"))
 
+(defconst isar-keywords-theory-script
+  '("declare"
+    "inductive_cases"))
+
 (defconst isar-keywords-theory-goal
   '("instance"
     "lemma"
-- 
cgit v1.2.3