diff -r 1bebf8007677 -r b1d64b7ce2b7 isar-keywords-quot.el --- 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"