this version actually generated by Isabelle;

1 files changed, 40 insertions, 58 deletions

diff --git a/isar/isar-keywords.el b/isar/isar-keywords.el
index 53e40c8f..4d5c1694 100644
--- a/isar/isar-keywords.el
+++ b/isar/isar-keywords.el
@@ -1,24 +1,30 @@
 ;;
-;; Keyword classification for Isabelle/Isar.
-;; File generated by Isabelle -- DO NOT EDIT!
+;; Keyword classification tables for Isabelle/Isar.
+;; This file generated by Isabelle -- DO NOT EDIT!
 ;;
 ;; $Id$
 ;;
 
 (defconst isar-keywords-minor
-  '(
-    "and"
+  '("and"
     "as"
     "binder"
+    "con_defs"
+    "congs"
+    "distinct"
+    "files"
+    "induction"
     "infixl"
     "infixr"
+    "inject"
+    "intrs"
     "is"
+    "monos"
     "output"
-    ))
+    "simpset"))
 
 (defconst isar-keywords-control
-  '(
-    "break"
+  '("break"
     "cd"
     "clear_undo"
     "exit"
@@ -31,12 +37,10 @@
     "top"
     "undo"
     "undos"
-    "up"
-    ))
+    "up"))
 
 (defconst isar-keywords-diag
-  '(
-    "ML"
+  '("ML"
     "commit"
     "help"
     "pr"
@@ -53,33 +57,27 @@
     "thm"
     "typ"
     "update_thy"
-    "use" 
+    "use"
     "use_thy"
-    ))
+    "use_thy_only"))
 
 (defconst isar-keywords-theory-begin
-  '(
-    "context"
+  '("context"
     "theory"
-    "update_context"
-    ))
+    "update_context"))
 
 (defconst isar-keywords-theory-end
-  '(
-    "end"
-    ))
+  '("end"))
 
 (defconst isar-keywords-theory-heading
-  '(
-    "chapter"
+  '("chapter"
     "section"
     "subsection"
     "subsubsection"
-    ))
+    "title"))
 
 (defconst isar-keywords-theory-decl
-  '(
-    "arities"
+  '("arities"
     "axclass"
     "axioms"
     "classes"
@@ -110,66 +108,50 @@
     "syntax"
     "text"
     "theorems"
-    "title"
     "token_translation"
     "translations"
     "typed_print_translation"
     "typedecl"
-    "types"
-    ))
+    "types"))
 
 (defconst isar-keywords-theory-goal
-  '(
-    "typedef"
-    "theorem"
+  '("instance"
     "lemma"
-    "instance"
-    ))
+    "theorem"
+    "typedef"))
 
 (defconst isar-keywords-qed
-  '(
-    "\\."
+  '("\\."
     "\\.\\."
     "by"
     "qed"
-    "qed_with"
-    ))
+    "qed_with"))
 
 (defconst isar-keywords-proof-goal
-  '(
-    "have"
+  '("have"
     "hence"
     "show"
-    "thus"
-    ))
+    "thus"))
 
 (defconst isar-keywords-proof-block
-  '(
-    "next"
-    "proof" 
+  '("next"
+    "proof"
     "{{"
-    "}}"
-    ))
+    "}}"))
 
 (defconst isar-keywords-proof-chain
-  '(
-    "then"
-    "from"
-    ))
+  '("from"
+    "then"))
 
 (defconst isar-keywords-proof-decl
-  '(
-    "assume"
+  '("assume"
     "fix"
     "let"
-    "note"
-    ))
+    "note"))
 
 (defconst isar-keywords-proof-script
-  '(
-    "back"
+  '("back"
     "refine"
-    "then_refine"
-    ))
+    "then_refine"))
 
 (provide 'isar-keywords)