--- a/src/HOL/IsaMakefile Tue Nov 03 14:51:55 2009 +0100
+++ b/src/HOL/IsaMakefile Tue Nov 03 17:54:24 2009 +0100
@@ -10,6 +10,7 @@
images: \
HOL \
HOL-Algebra \
+ HOL-Boogie \
HOL-Base \
HOL-Main \
HOL-Multivariate_Analysis \
@@ -27,6 +28,7 @@
HOL-ex \
HOL-Auth \
HOL-Bali \
+ HOL-Boogie_Examples \
HOL-Decision_Procs \
HOL-Extraction \
HOL-Hahn_Banach \
@@ -54,7 +56,7 @@
HOL-Probability \
HOL-Prolog \
HOL-SET_Protocol \
- HOL-SMT-Examples \
+ HOL-SMT_Examples \
HOL-SizeChange \
HOL-Statespace \
HOL-Subst \
@@ -1212,7 +1214,7 @@
HOL-SMT: HOL-Word $(OUT)/HOL-SMT
-$(OUT)/HOL-SMT: $(OUT)/HOL-Word SMT/SMT_Base.thy SMT/Z3.thy \
+$(OUT)/HOL-SMT: $(OUT)/HOL-Word SMT/ROOT.ML SMT/SMT_Base.thy SMT/Z3.thy \
SMT/SMT.thy SMT/Tools/smt_normalize.ML SMT/Tools/smt_monomorph.ML \
SMT/Tools/smt_translate.ML SMT/Tools/smtlib_interface.ML \
SMT/Tools/smt_solver.ML SMT/Tools/cvc3_solver.ML \
@@ -1222,11 +1224,11 @@
@cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT
-## HOL-SMT-Examples
+## HOL-SMT_Examples
-HOL-SMT-Examples: HOL-SMT $(LOG)/HOL-SMT-Examples.gz
+HOL-SMT_Examples: HOL-SMT $(LOG)/HOL-SMT_Examples.gz
-$(LOG)/HOL-SMT-Examples.gz: $(OUT)/HOL-SMT SMT/Examples/ROOT.ML \
+$(LOG)/HOL-SMT_Examples.gz: $(OUT)/HOL-SMT SMT/Examples/ROOT.ML \
SMT/Examples/SMT_Examples.thy SMT/Examples/cert/z3_arith_quant_01 \
SMT/Examples/cert/z3_arith_quant_01.proof \
SMT/Examples/cert/z3_arith_quant_02 \
@@ -1381,6 +1383,33 @@
@cd SMT; $(ISABELLE_TOOL) usedir $(OUT)/HOL-SMT Examples
+## HOL-Boogie
+
+HOL-Boogie: HOL-SMT $(OUT)/HOL-Boogie
+
+$(OUT)/HOL-Boogie: $(OUT)/HOL-SMT Boogie/ROOT.ML Boogie/Boogie.thy \
+ Boogie/Tools/boogie_vcs.ML Boogie/Tools/boogie_loader.ML \
+ Boogie/Tools/boogie_commands.ML Boogie/Tools/boogie_split.ML
+ @cd Boogie; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-SMT HOL-Boogie
+
+
+## HOL-Boogie_Examples
+
+HOL-Boogie_Examples: HOL-Boogie $(LOG)/HOL-Boogie_Examples.gz
+
+$(LOG)/HOL-Boogie_Examples.gz: $(OUT)/HOL-SMT Boogie/Examples/ROOT.ML \
+ Boogie/Examples/Boogie_Max.thy Boogie/Examples/Boogie_Max.b2i \
+ Boogie/Examples/Boogie_Dijkstra.thy Boogie/Examples/VCC_Max.thy \
+ Boogie/Examples/Boogie_Dijkstra.b2i Boogie/Examples/VCC_Max.b2i \
+ Boogie/Examples/cert/Boogie_b_max \
+ Boogie/Examples/cert/Boogie_b_max.proof \
+ Boogie/Examples/cert/Boogie_b_Dijkstra \
+ Boogie/Examples/cert/Boogie_b_Dijkstra.proof \
+ Boogie/Examples/cert/VCC_b_maximum \
+ Boogie/Examples/cert/VCC_b_maximum.proof
+ @cd Boogie; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Boogie Examples
+
+
## clean
clean: