--- a/isar-keywords-quot.el Fri May 07 12:10:04 2010 +0200
+++ b/isar-keywords-quot.el Fri May 07 12:28:11 2010 +0200
@@ -61,6 +61,7 @@
"code_modulename"
"code_monad"
"code_pred"
+ "code_reflect"
"code_reserved"
"code_thms"
"code_type"
@@ -76,7 +77,7 @@
"declaration"
"declare"
"def"
- "defaultsort"
+ "default_sort"
"defer"
"defer_recdef"
"definition"
@@ -106,7 +107,10 @@
"header"
"help"
"hence"
- "hide"
+ "hide_class"
+ "hide_const"
+ "hide_fact"
+ "hide_type"
"inductive"
"inductive_cases"
"inductive_set"
@@ -205,12 +209,18 @@
"refute_params"
"remove_thy"
"rep_datatype"
+ "repdef"
+ "schematic_corollary"
+ "schematic_lemma"
+ "schematic_theorem"
"sect"
"section"
"setup"
"show"
"simproc_setup"
"sledgehammer"
+ "sledgehammer_params"
+ "smt_status"
"sorry"
"specification"
"subclass"
@@ -433,6 +443,7 @@
"code_module"
"code_modulename"
"code_monad"
+ "code_reflect"
"code_reserved"
"code_type"
"coinductive"
@@ -454,7 +465,10 @@
"finalconsts"
"fun"
"global"
- "hide"
+ "hide_class"
+ "hide_const"
+ "hide_fact"
+ "hide_type"
"inductive"
"inductive_set"
"instantiation"
@@ -487,6 +501,8 @@
"refute_params"
"setup"
"simproc_setup"
+ "sledgehammer_params"
+ "statespace"
"syntax"
"text"
"text_raw"
@@ -516,6 +532,9 @@
"quotient_type"
"recdef_tc"
"rep_datatype"
+ "schematic_corollary"
+ "schematic_lemma"
+ "schematic_theorem"
"specification"
"subclass"
"sublocale"