isar-keywords-quot.el
changeset 2079 b1d64b7ce2b7
parent 777 2f72662d21f3
--- 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"