--- a/Admin/update-keywords Sat Nov 14 18:36:05 2009 +0100
+++ b/Admin/update-keywords Sat Nov 14 18:45:24 2009 +0100
@@ -12,7 +12,7 @@
isabelle keywords \
"$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" \
- "$LOG/IOA.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz"
+ "$LOG/IOA.gz" "$LOG/HOL-Boogie.gz" "$LOG/HOL-Nominal.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 Sat Nov 14 18:36:05 2009 +0100
+++ b/etc/isar-keywords.el Sat Nov 14 18:45:24 2009 +0100
@@ -1,6 +1,6 @@
;;
;; Keyword classification tables for Isabelle/Isar.
-;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Nominal + HOL-Statespace.
+;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Boogie + HOL-Nominal + HOL-Statespace.
;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
;;
@@ -40,6 +40,10 @@
"axiomatization"
"axioms"
"back"
+ "boogie_end"
+ "boogie_open"
+ "boogie_status"
+ "boogie_vc"
"by"
"cannot_undo"
"case"
@@ -343,6 +347,7 @@
"atp_kill"
"atp_messages"
"atp_minimize"
+ "boogie_status"
"cd"
"class_deps"
"code_deps"
@@ -434,6 +439,8 @@
"axclass"
"axiomatization"
"axioms"
+ "boogie_end"
+ "boogie_open"
"class"
"classes"
"classrel"
@@ -520,6 +527,7 @@
(defconst isar-keywords-theory-goal
'("ax_specification"
+ "boogie_vc"
"code_pred"
"corollary"
"cpodef"