# HG changeset patch
# User wenzelm
# Date 1258220724 -3600
# Node ID 3222fa0528466d77f5905bdfa0a9523027c910e2
# Parent  8e33ca8832b144681b4646a9b85ada2b4369f6c2
include HOL-Boogie keywords by default;

diff -r 8e33ca8832b1 -r 3222fa052846 Admin/update-keywords
--- 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"
diff -r 8e33ca8832b1 -r 3222fa052846 etc/isar-keywords.el
--- 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"