1.1 --- a/src/HOL/IsaMakefile Tue Nov 03 14:51:55 2009 +0100
1.2 +++ b/src/HOL/IsaMakefile Tue Nov 03 17:54:24 2009 +0100
1.3 @@ -10,6 +10,7 @@
1.4 images: \
1.5 HOL \
1.6 HOL-Algebra \
1.7 + HOL-Boogie \
1.8 HOL-Base \
1.9 HOL-Main \
1.10 HOL-Multivariate_Analysis \
1.11 @@ -27,6 +28,7 @@
1.12 HOL-ex \
1.13 HOL-Auth \
1.14 HOL-Bali \
1.15 + HOL-Boogie_Examples \
1.16 HOL-Decision_Procs \
1.17 HOL-Extraction \
1.18 HOL-Hahn_Banach \
1.19 @@ -54,7 +56,7 @@
1.20 HOL-Probability \
1.21 HOL-Prolog \
1.22 HOL-SET_Protocol \
1.23 - HOL-SMT-Examples \
1.24 + HOL-SMT_Examples \
1.25 HOL-SizeChange \
1.26 HOL-Statespace \
1.27 HOL-Subst \
1.28 @@ -1212,7 +1214,7 @@
1.29
1.30 HOL-SMT: HOL-Word $(OUT)/HOL-SMT
1.31
1.32 -$(OUT)/HOL-SMT: $(OUT)/HOL-Word SMT/SMT_Base.thy SMT/Z3.thy \
1.33 +$(OUT)/HOL-SMT: $(OUT)/HOL-Word SMT/ROOT.ML SMT/SMT_Base.thy SMT/Z3.thy \
1.34 SMT/SMT.thy SMT/Tools/smt_normalize.ML SMT/Tools/smt_monomorph.ML \
1.35 SMT/Tools/smt_translate.ML SMT/Tools/smtlib_interface.ML \
1.36 SMT/Tools/smt_solver.ML SMT/Tools/cvc3_solver.ML \
1.37 @@ -1222,11 +1224,11 @@
1.38 @cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT
1.39
1.40
1.41 -## HOL-SMT-Examples
1.42 +## HOL-SMT_Examples
1.43
1.44 -HOL-SMT-Examples: HOL-SMT $(LOG)/HOL-SMT-Examples.gz
1.45 +HOL-SMT_Examples: HOL-SMT $(LOG)/HOL-SMT_Examples.gz
1.46
1.47 -$(LOG)/HOL-SMT-Examples.gz: $(OUT)/HOL-SMT SMT/Examples/ROOT.ML \
1.48 +$(LOG)/HOL-SMT_Examples.gz: $(OUT)/HOL-SMT SMT/Examples/ROOT.ML \
1.49 SMT/Examples/SMT_Examples.thy SMT/Examples/cert/z3_arith_quant_01 \
1.50 SMT/Examples/cert/z3_arith_quant_01.proof \
1.51 SMT/Examples/cert/z3_arith_quant_02 \
1.52 @@ -1381,6 +1383,33 @@
1.53 @cd SMT; $(ISABELLE_TOOL) usedir $(OUT)/HOL-SMT Examples
1.54
1.55
1.56 +## HOL-Boogie
1.57 +
1.58 +HOL-Boogie: HOL-SMT $(OUT)/HOL-Boogie
1.59 +
1.60 +$(OUT)/HOL-Boogie: $(OUT)/HOL-SMT Boogie/ROOT.ML Boogie/Boogie.thy \
1.61 + Boogie/Tools/boogie_vcs.ML Boogie/Tools/boogie_loader.ML \
1.62 + Boogie/Tools/boogie_commands.ML Boogie/Tools/boogie_split.ML
1.63 + @cd Boogie; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-SMT HOL-Boogie
1.64 +
1.65 +
1.66 +## HOL-Boogie_Examples
1.67 +
1.68 +HOL-Boogie_Examples: HOL-Boogie $(LOG)/HOL-Boogie_Examples.gz
1.69 +
1.70 +$(LOG)/HOL-Boogie_Examples.gz: $(OUT)/HOL-SMT Boogie/Examples/ROOT.ML \
1.71 + Boogie/Examples/Boogie_Max.thy Boogie/Examples/Boogie_Max.b2i \
1.72 + Boogie/Examples/Boogie_Dijkstra.thy Boogie/Examples/VCC_Max.thy \
1.73 + Boogie/Examples/Boogie_Dijkstra.b2i Boogie/Examples/VCC_Max.b2i \
1.74 + Boogie/Examples/cert/Boogie_b_max \
1.75 + Boogie/Examples/cert/Boogie_b_max.proof \
1.76 + Boogie/Examples/cert/Boogie_b_Dijkstra \
1.77 + Boogie/Examples/cert/Boogie_b_Dijkstra.proof \
1.78 + Boogie/Examples/cert/VCC_b_maximum \
1.79 + Boogie/Examples/cert/VCC_b_maximum.proof
1.80 + @cd Boogie; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Boogie Examples
1.81 +
1.82 +
1.83 ## clean
1.84
1.85 clean: