# HG changeset patch
# User wenzelm
# Date 1414492077 -3600
# Node ID 944364b48eb908cf15f3f544cccd1c97dc295128
# Parent  49ed5eea15d48bef6d66945901648f9344219141
updated keywords;

diff -r 49ed5eea15d4 -r 944364b48eb9 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Tue Oct 28 10:35:38 2014 +0100
+++ b/etc/isar-keywords.el	Tue Oct 28 11:27:57 2014 +0100
@@ -1,6 +1,6 @@
 ;;
 ;; Keyword classification tables for Isabelle/Isar.
-;; Generated from HOL + HOL-Auth + HOL-BNF_Examples + HOL-Bali + HOL-Decision_Procs + HOL-IMP + HOL-Imperative_HOL + HOL-Import + HOL-Library + HOL-Mutabelle + HOL-Nominal + HOL-Predicate_Compile_Examples + HOL-Proofs + HOL-Proofs-Extraction + HOL-SPARK + HOL-Statespace + HOL-TPTP + HOL-Word-SMT_Examples + HOL-ex + HOLCF + Pure.
+;; Generated from HOL + HOL-Auth + HOL-Bali + HOL-Datatype_Examples + HOL-Decision_Procs + HOL-Hahn_Banach + HOL-IMP + HOL-Imperative_HOL + HOL-Import + HOL-Induct + HOL-Library + HOL-Multivariate_Analysis + HOL-Mutabelle + HOL-Nominal + HOL-Predicate_Compile_Examples + HOL-Probability + HOL-Proofs + HOL-Proofs-Extraction + HOL-SPARK + HOL-Statespace + HOL-TPTP + HOL-Word-SMT_Examples + HOL-ex + HOLCF + Pure.
 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
 ;;
 
@@ -65,7 +65,6 @@
     "cpodef"
     "datatype"
     "datatype_compat"
-    "datatype_new"
     "declaration"
     "declare"
     "def"
@@ -159,6 +158,9 @@
     "note"
     "notepad"
     "obtain"
+    "old_datatype"
+    "old_rep_datatype"
+    "old_smt_status"
     "oops"
     "oracle"
     "overloading"
@@ -235,7 +237,6 @@
     "refute"
     "refute_params"
     "remove_thy"
-    "rep_datatype"
     "schematic_corollary"
     "schematic_lemma"
     "schematic_theorem"
@@ -248,7 +249,6 @@
     "simps_of_case"
     "sledgehammer"
     "sledgehammer_params"
-    "smt2_status"
     "smt_status"
     "solve_direct"
     "sorry"
@@ -272,6 +272,7 @@
     "term"
     "term_cartouche"
     "termination"
+    "test_code"
     "text"
     "text_cartouche"
     "text_raw"
@@ -405,6 +406,7 @@
     "help"
     "locale_deps"
     "nitpick"
+    "old_smt_status"
     "pr"
     "prf"
     "print_ML_antiquotations"
@@ -452,12 +454,12 @@
     "quickcheck"
     "refute"
     "sledgehammer"
-    "smt2_status"
     "smt_status"
     "solve_direct"
     "spark_status"
     "term"
     "term_cartouche"
+    "test_code"
     "thm"
     "thm_deps"
     "thy_deps"
@@ -514,7 +516,6 @@
     "context"
     "datatype"
     "datatype_compat"
-    "datatype_new"
     "declaration"
     "declare"
     "default_sort"
@@ -562,6 +563,7 @@
     "nonterminal"
     "notation"
     "notepad"
+    "old_datatype"
     "oracle"
     "overloading"
     "parse_ast_translation"
@@ -621,13 +623,13 @@
     "nominal_inductive2"
     "nominal_primrec"
     "nominal_termination"
+    "old_rep_datatype"
     "pcpodef"
     "permanent_interpretation"
     "primcorecursive"
     "quotient_definition"
     "quotient_type"
     "recdef_tc"
-    "rep_datatype"
     "schematic_corollary"
     "schematic_lemma"
     "schematic_theorem"