src/HOL/IsaMakefile
changeset 33439 f5d95787224f
parent 33437 c8bc8dc5869f
child 33447 6895b9cadc7c
child 33448 7f716a975ada
     1.1 --- a/src/HOL/IsaMakefile	Thu Nov 05 13:57:56 2009 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Thu Nov 05 14:37:39 2009 +0100
     1.3 @@ -28,7 +28,7 @@
     1.4    HOL-ex \
     1.5    HOL-Auth \
     1.6    HOL-Bali \
     1.7 -  HOL-Boogie_Examples \
     1.8 +  HOL-Boogie-Examples \
     1.9    HOL-Decision_Procs \
    1.10    HOL-Extraction \
    1.11    HOL-Hahn_Banach \
    1.12 @@ -56,7 +56,7 @@
    1.13    HOL-Probability \
    1.14    HOL-Prolog \
    1.15    HOL-SET_Protocol \
    1.16 -  HOL-SMT_Examples \
    1.17 +  HOL-SMT-Examples \
    1.18    HOL-SizeChange \
    1.19    HOL-Statespace \
    1.20    HOL-Subst \
    1.21 @@ -581,16 +581,15 @@
    1.22  HOL-Hoare_Parallel: HOL $(LOG)/HOL-Hoare_Parallel.gz
    1.23  
    1.24  $(LOG)/HOL-Hoare_Parallel.gz: $(OUT)/HOL Hoare_Parallel/Gar_Coll.thy	\
    1.25 -  Hoare_Parallel/Graph.thy Hoare_Parallel/Hoare_Parallel.thy	\
    1.26 -  Hoare_Parallel/Mul_Gar_Coll.thy		\
    1.27 -  Hoare_Parallel/OG_Com.thy Hoare_Parallel/OG_Examples.thy		\
    1.28 -  Hoare_Parallel/OG_Hoare.thy Hoare_Parallel/OG_Syntax.thy		\
    1.29 -  Hoare_Parallel/OG_Tactics.thy Hoare_Parallel/OG_Tran.thy		\
    1.30 -  Hoare_Parallel/Quote_Antiquote.thy Hoare_Parallel/RG_Com.thy		\
    1.31 -  Hoare_Parallel/RG_Examples.thy Hoare_Parallel/RG_Hoare.thy		\
    1.32 -  Hoare_Parallel/RG_Syntax.thy Hoare_Parallel/RG_Tran.thy			\
    1.33 -  Hoare_Parallel/ROOT.ML Hoare_Parallel/document/root.tex			\
    1.34 -  Hoare_Parallel/document/root.bib
    1.35 +  Hoare_Parallel/Graph.thy Hoare_Parallel/Hoare_Parallel.thy		\
    1.36 +  Hoare_Parallel/Mul_Gar_Coll.thy Hoare_Parallel/OG_Com.thy		\
    1.37 +  Hoare_Parallel/OG_Examples.thy Hoare_Parallel/OG_Hoare.thy		\
    1.38 +  Hoare_Parallel/OG_Syntax.thy Hoare_Parallel/OG_Tactics.thy		\
    1.39 +  Hoare_Parallel/OG_Tran.thy Hoare_Parallel/Quote_Antiquote.thy		\
    1.40 +  Hoare_Parallel/RG_Com.thy Hoare_Parallel/RG_Examples.thy		\
    1.41 +  Hoare_Parallel/RG_Hoare.thy Hoare_Parallel/RG_Syntax.thy		\
    1.42 +  Hoare_Parallel/RG_Tran.thy Hoare_Parallel/ROOT.ML			\
    1.43 +  Hoare_Parallel/document/root.tex Hoare_Parallel/document/root.bib
    1.44  	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hoare_Parallel
    1.45  
    1.46  
    1.47 @@ -610,20 +609,20 @@
    1.48  
    1.49  HOL-Nitpick_Examples: HOL $(LOG)/HOL-Nitpick_Examples.gz
    1.50  
    1.51 -$(LOG)/HOL-Nitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML \
    1.52 -  Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy \
    1.53 -  Nitpick_Examples/Induct_Nits.thy Nitpick_Examples/Manual_Nits.thy \
    1.54 -  Nitpick_Examples/Mini_Nits.thy Nitpick_Examples/Mono_Nits.thy \
    1.55 -  Nitpick_Examples/Nitpick_Examples.thy Nitpick_Examples/Pattern_Nits.thy \
    1.56 -  Nitpick_Examples/Record_Nits.thy Nitpick_Examples/Refute_Nits.thy \
    1.57 -  Nitpick_Examples/Special_Nits.thy Nitpick_Examples/Tests_Nits.thy \
    1.58 -  Nitpick_Examples/Typedef_Nits.thy
    1.59 +$(LOG)/HOL-Nitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML	\
    1.60 +  Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy	\
    1.61 +  Nitpick_Examples/Induct_Nits.thy Nitpick_Examples/Manual_Nits.thy	\
    1.62 +  Nitpick_Examples/Mini_Nits.thy Nitpick_Examples/Mono_Nits.thy		\
    1.63 +  Nitpick_Examples/Nitpick_Examples.thy					\
    1.64 +  Nitpick_Examples/Pattern_Nits.thy Nitpick_Examples/Record_Nits.thy	\
    1.65 +  Nitpick_Examples/Refute_Nits.thy Nitpick_Examples/Special_Nits.thy	\
    1.66 +  Nitpick_Examples/Tests_Nits.thy Nitpick_Examples/Typedef_Nits.thy
    1.67  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Nitpick_Examples
    1.68  
    1.69  
    1.70  ## HOL-Algebra
    1.71  
    1.72 -HOL-Algebra: HOL $(LOG)/HOL-Algebra.gz
    1.73 +HOL-Algebra: HOL $(OUT)/HOL-Algebra
    1.74  
    1.75  ALGEBRA_DEPENDENCIES = $(OUT)/HOL \
    1.76    Algebra/ROOT.ML \
    1.77 @@ -701,8 +700,8 @@
    1.78  HOL-UNITY: HOL $(LOG)/HOL-UNITY.gz
    1.79  
    1.80  $(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML	\
    1.81 -  UNITY/UNITY_Main.thy UNITY/UNITY_Examples.thy UNITY/UNITY_tactics.ML UNITY/Comp.thy		\
    1.82 -  UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy			\
    1.83 +  UNITY/UNITY_Main.thy UNITY/UNITY_Examples.thy UNITY/UNITY_tactics.ML	\
    1.84 +  UNITY/Comp.thy UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy	\
    1.85    UNITY/Extend.thy UNITY/FP.thy UNITY/Follows.thy UNITY/Guar.thy	\
    1.86    UNITY/Lift_prog.thy UNITY/ListOrder.thy UNITY/ProgressSets.thy	\
    1.87    UNITY/PPROD.thy UNITY/Project.thy UNITY/Rename.thy			\
    1.88 @@ -942,7 +941,7 @@
    1.89  
    1.90  HOL-ex: HOL $(LOG)/HOL-ex.gz
    1.91  
    1.92 -$(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy		\
    1.93 +$(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy	\
    1.94    Number_Theory/Primes.thy						\
    1.95    Tools/Predicate_Compile/predicate_compile_core.ML			\
    1.96    ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy		\
    1.97 @@ -950,22 +949,21 @@
    1.98    ex/Binary.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy		\
    1.99    ex/CodegenSML_Test.thy ex/Codegenerator_Candidates.thy		\
   1.100    ex/Codegenerator_Pretty.thy ex/Codegenerator_Pretty_Test.thy		\
   1.101 -  ex/Codegenerator_Test.thy ex/Coherent.thy	\
   1.102 -  ex/Efficient_Nat_examples.thy	\
   1.103 -  ex/Eval_Examples.thy ex/Fundefs.thy ex/Groebner_Examples.thy		\
   1.104 -  ex/Guess.thy ex/HarmonicSeries.thy ex/Hebrew.thy			\
   1.105 -  ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy			\
   1.106 +  ex/Codegenerator_Test.thy ex/Coherent.thy				\
   1.107 +  ex/Efficient_Nat_examples.thy ex/Eval_Examples.thy ex/Fundefs.thy	\
   1.108 +  ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy		\
   1.109 +  ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy	\
   1.110    ex/Hilbert_Classical.thy ex/Induction_Scheme.thy			\
   1.111    ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy		\
   1.112    ex/Intuitionistic.thy ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy	\
   1.113    ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy			\
   1.114    ex/Multiquote.thy ex/NatSum.thy ex/Numeral.thy ex/PER.thy		\
   1.115 -  ex/Predicate_Compile_ex.thy ex/Predicate_Compile_Quickcheck.thy			\
   1.116 +  ex/Predicate_Compile_ex.thy ex/Predicate_Compile_Quickcheck.thy	\
   1.117    ex/PresburgerEx.thy ex/Primrec.thy ex/Quickcheck_Examples.thy		\
   1.118    ex/ROOT.ML ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy		\
   1.119    ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
   1.120    ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy		\
   1.121 -  ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy ex/Tree23.thy     \
   1.122 +  ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy ex/Tree23.thy	\
   1.123    ex/Unification.thy ex/document/root.bib ex/document/root.tex		\
   1.124    ex/set.thy ex/svc_funcs.ML ex/svc_test.thy
   1.125  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
   1.126 @@ -1065,12 +1063,13 @@
   1.127  
   1.128  HOL-Multivariate_Analysis: HOL $(OUT)/HOL-Multivariate_Analysis
   1.129  
   1.130 -$(OUT)/HOL-Multivariate_Analysis: $(OUT)/HOL Multivariate_Analysis/ROOT.ML \
   1.131 -  Multivariate_Analysis/Multivariate_Analysis.thy \
   1.132 -  Multivariate_Analysis/Determinants.thy \
   1.133 -  Multivariate_Analysis/Finite_Cartesian_Product.thy \
   1.134 -  Multivariate_Analysis/Euclidean_Space.thy \
   1.135 -  Multivariate_Analysis/Topology_Euclidean_Space.thy \
   1.136 +$(OUT)/HOL-Multivariate_Analysis: $(OUT)/HOL		\
   1.137 +  Multivariate_Analysis/ROOT.ML				\
   1.138 +  Multivariate_Analysis/Multivariate_Analysis.thy	\
   1.139 +  Multivariate_Analysis/Determinants.thy		\
   1.140 +  Multivariate_Analysis/Finite_Cartesian_Product.thy	\
   1.141 +  Multivariate_Analysis/Euclidean_Space.thy		\
   1.142 +  Multivariate_Analysis/Topology_Euclidean_Space.thy	\
   1.143    Multivariate_Analysis/Convex_Euclidean_Space.thy
   1.144  	@cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Multivariate_Analysis
   1.145  
   1.146 @@ -1224,11 +1223,11 @@
   1.147  	@cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT
   1.148  
   1.149  
   1.150 -## HOL-SMT_Examples
   1.151 +## HOL-SMT-Examples
   1.152  
   1.153 -HOL-SMT_Examples: HOL-SMT $(LOG)/HOL-SMT_Examples.gz
   1.154 +HOL-SMT-Examples: HOL-SMT $(LOG)/HOL-SMT-Examples.gz
   1.155  
   1.156 -$(LOG)/HOL-SMT_Examples.gz: $(OUT)/HOL-SMT SMT/Examples/ROOT.ML		\
   1.157 +$(LOG)/HOL-SMT-Examples.gz: $(OUT)/HOL-SMT SMT/Examples/ROOT.ML		\
   1.158    SMT/Examples/SMT_Examples.thy SMT/Examples/cert/z3_arith_quant_01	\
   1.159    SMT/Examples/cert/z3_arith_quant_01.proof				\
   1.160    SMT/Examples/cert/z3_arith_quant_02					\
   1.161 @@ -1387,25 +1386,25 @@
   1.162  
   1.163  HOL-Boogie: HOL-SMT $(OUT)/HOL-Boogie
   1.164  
   1.165 -$(OUT)/HOL-Boogie: $(OUT)/HOL-SMT Boogie/ROOT.ML Boogie/Boogie.thy      \
   1.166 -  Boogie/Tools/boogie_vcs.ML Boogie/Tools/boogie_loader.ML              \
   1.167 +$(OUT)/HOL-Boogie: $(OUT)/HOL-SMT Boogie/ROOT.ML Boogie/Boogie.thy	\
   1.168 +  Boogie/Tools/boogie_vcs.ML Boogie/Tools/boogie_loader.ML		\
   1.169    Boogie/Tools/boogie_commands.ML Boogie/Tools/boogie_split.ML
   1.170  	@cd Boogie; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-SMT HOL-Boogie
   1.171  
   1.172  
   1.173  ## HOL-Boogie_Examples
   1.174  
   1.175 -HOL-Boogie_Examples: HOL-Boogie $(LOG)/HOL-Boogie_Examples.gz
   1.176 +HOL-Boogie-Examples: HOL-Boogie $(LOG)/HOL-Boogie-Examples.gz
   1.177  
   1.178 -$(LOG)/HOL-Boogie_Examples.gz: $(OUT)/HOL-SMT Boogie/Examples/ROOT.ML   \
   1.179 -  Boogie/Examples/Boogie_Max.thy Boogie/Examples/Boogie_Max.b2i         \
   1.180 -  Boogie/Examples/Boogie_Dijkstra.thy Boogie/Examples/VCC_Max.thy       \
   1.181 -  Boogie/Examples/Boogie_Dijkstra.b2i Boogie/Examples/VCC_Max.b2i       \
   1.182 -  Boogie/Examples/cert/Boogie_b_max                                     \
   1.183 -  Boogie/Examples/cert/Boogie_b_max.proof                               \
   1.184 -  Boogie/Examples/cert/Boogie_b_Dijkstra                                \
   1.185 -  Boogie/Examples/cert/Boogie_b_Dijkstra.proof                          \
   1.186 -  Boogie/Examples/cert/VCC_b_maximum                                    \
   1.187 +$(LOG)/HOL-Boogie-Examples.gz: $(OUT)/HOL-Boogie			\
   1.188 +  Boogie/Examples/ROOT.ML Boogie/Examples/Boogie_Max.thy		\
   1.189 +  Boogie/Examples/Boogie_Max.b2i Boogie/Examples/Boogie_Dijkstra.thy	\
   1.190 +  Boogie/Examples/VCC_Max.thy Boogie/Examples/Boogie_Dijkstra.b2i	\
   1.191 +  Boogie/Examples/VCC_Max.b2i Boogie/Examples/cert/Boogie_b_max		\
   1.192 +  Boogie/Examples/cert/Boogie_b_max.proof				\
   1.193 +  Boogie/Examples/cert/Boogie_b_Dijkstra				\
   1.194 +  Boogie/Examples/cert/Boogie_b_Dijkstra.proof				\
   1.195 +  Boogie/Examples/cert/VCC_b_maximum					\
   1.196    Boogie/Examples/cert/VCC_b_maximum.proof
   1.197  	@cd Boogie; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Boogie Examples
   1.198  
   1.199 @@ -1434,5 +1433,7 @@
   1.200  		$(LOG)/HOL-Word-Examples.gz $(OUT)/HOL-NSA		\
   1.201  		$(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz		\
   1.202  		$(LOG)/HOL-Mirabelle.gz $(OUT)/HOL-SMT			\
   1.203 -		$(LOG)/HOL-SMT.gz $(LOG)/HOL-SMT-Examples.gz
   1.204 +		$(LOG)/HOL-SMT.gz $(LOG)/HOL-SMT-Examples.gz 		\
   1.205 +		$(OUT)/HOL-Boogie $(LOG)/HOL-Boogie.gz 			\
   1.206 +		$(LOG)/HOL-Boogie-Examples.gz
   1.207