1.1 --- a/Admin/update-keywords	Sat Nov 14 18:36:05 2009 +0100
     1.2 +++ b/Admin/update-keywords	Sat Nov 14 18:45:24 2009 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4  
     1.5  isabelle keywords \
     1.6    "$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" \
     1.7 -  "$LOG/IOA.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz"
     1.8 +  "$LOG/IOA.gz" "$LOG/HOL-Boogie.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz"
     1.9  
    1.10  isabelle keywords -k ZF \
    1.11    "$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/FOL.gz" "$LOG/ZF.gz"

     2.1 --- a/etc/isar-keywords.el	Sat Nov 14 18:36:05 2009 +0100
     2.2 +++ b/etc/isar-keywords.el	Sat Nov 14 18:45:24 2009 +0100
     2.3 @@ -1,6 +1,6 @@
     2.4  ;;
     2.5  ;; Keyword classification tables for Isabelle/Isar.
     2.6 -;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Nominal + HOL-Statespace.
     2.7 +;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Boogie + HOL-Nominal + HOL-Statespace.
     2.8  ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
     2.9  ;;
    2.10  
    2.11 @@ -40,6 +40,10 @@
    2.12      "axiomatization"
    2.13      "axioms"
    2.14      "back"
    2.15 +    "boogie_end"
    2.16 +    "boogie_open"
    2.17 +    "boogie_status"
    2.18 +    "boogie_vc"
    2.19      "by"
    2.20      "cannot_undo"
    2.21      "case"
    2.22 @@ -343,6 +347,7 @@
    2.23      "atp_kill"
    2.24      "atp_messages"
    2.25      "atp_minimize"
    2.26 +    "boogie_status"
    2.27      "cd"
    2.28      "class_deps"
    2.29      "code_deps"
    2.30 @@ -434,6 +439,8 @@
    2.31      "axclass"
    2.32      "axiomatization"
    2.33      "axioms"
    2.34 +    "boogie_end"
    2.35 +    "boogie_open"
    2.36      "class"
    2.37      "classes"
    2.38      "classrel"
    2.39 @@ -520,6 +527,7 @@
    2.40  
    2.41  (defconst isar-keywords-theory-goal
    2.42    '("ax_specification"
    2.43 +    "boogie_vc"
    2.44      "code_pred"
    2.45      "corollary"
    2.46      "cpodef"