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