--- a/Admin/update-keywords Wed Nov 25 15:04:20 2009 +0100
+++ b/Admin/update-keywords Wed Nov 25 15:21:41 2009 +0100
@@ -12,7 +12,8 @@
isabelle keywords \
"$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" \
- "$LOG/IOA.gz" "$LOG/HOL-Boogie.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz"
+ "$LOG/IOA.gz" "$LOG/HOL-Boogie.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-SMT.gz" \
+ "$LOG/HOL-Statespace.gz"
isabelle keywords -k ZF \
"$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/FOL.gz" "$LOG/ZF.gz"
--- a/etc/isar-keywords.el Wed Nov 25 15:04:20 2009 +0100
+++ b/etc/isar-keywords.el Wed Nov 25 15:21:41 2009 +0100
@@ -1,6 +1,6 @@
;;
;; Keyword classification tables for Isabelle/Isar.
-;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Boogie + HOL-Nominal + HOL-Statespace.
+;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Boogie + HOL-Nominal + HOL-SMT + HOL-Statespace.
;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
;;
@@ -218,6 +218,7 @@
"show"
"simproc_setup"
"sledgehammer"
+ "smt_status"
"sorry"
"specification"
"statespace"
@@ -406,6 +407,7 @@
"refute"
"remove_thy"
"sledgehammer"
+ "smt_status"
"term"
"thm"
"thm_deps"