src/HOL/IsaMakefile
changeset 33419 8ae45e87b992
parent 33356 9157d0f9f00e
child 33437 c8bc8dc5869f
     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: