--- 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"