1.1 --- a/src/HOL/IsaMakefile Mon Sep 06 13:22:11 2010 +0200
1.2 +++ b/src/HOL/IsaMakefile Mon Sep 06 14:18:16 2010 +0200
1.3 @@ -57,6 +57,7 @@
1.4 HOL-Quotient_Examples \
1.5 HOL-Predicate_Compile_Examples \
1.6 HOL-Prolog \
1.7 + HOL-Proofs-ex \
1.8 HOL-Proofs-Extraction \
1.9 HOL-Proofs-Lambda \
1.10 HOL-SET_Protocol \
1.11 @@ -92,8 +93,6 @@
1.12
1.13 HOL-Main: Pure $(OUT)/HOL-Main
1.14
1.15 -HOL-Proofs: Pure $(OUT)/HOL-Proofs
1.16 -
1.17 Pure:
1.18 @cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
1.19
1.20 @@ -145,7 +144,7 @@
1.21 $(OUT)/HOL-Base: base.ML $(BASE_DEPENDENCIES)
1.22 @$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base
1.23
1.24 -PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES)\
1.25 +PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES) \
1.26 Complete_Lattice.thy \
1.27 Datatype.thy \
1.28 Extraction.thy \
1.29 @@ -355,9 +354,6 @@
1.30 $(OUT)/HOL-Main: main.ML $(MAIN_DEPENDENCIES)
1.31 @$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
1.32
1.33 -$(OUT)/HOL-Proofs: main.ML $(MAIN_DEPENDENCIES)
1.34 - @$(ISABELLE_TOOL) usedir -b -f main.ML -g true -p 2 -q 0 $(OUT)/Pure HOL-Proofs
1.35 -
1.36 HOL_DEPENDENCIES = $(MAIN_DEPENDENCIES) \
1.37 Archimedean_Field.thy \
1.38 Complex.thy \
1.39 @@ -390,7 +386,6 @@
1.40 @$(ISABELLE_TOOL) usedir -b -g true $(OUT)/Pure HOL
1.41
1.42
1.43 -
1.44 ## HOL-Library
1.45
1.46 HOL-Library: HOL $(OUT)/HOL-Library
1.47 @@ -855,17 +850,52 @@
1.48 @$(ISABELLE_TOOL) usedir -D generated $(OUT)/HOL Docs
1.49
1.50
1.51 +## HOL-Proofs
1.52 +
1.53 +HOL-Proofs: Pure $(OUT)/HOL-Proofs
1.54 +
1.55 +$(OUT)/HOL-Proofs: main.ML $(MAIN_DEPENDENCIES)
1.56 + @$(ISABELLE_TOOL) usedir -b -f main.ML -g true -p 2 -q 0 $(OUT)/Pure HOL-Proofs
1.57 +
1.58 +
1.59 +## HOL-Proofs-ex
1.60 +
1.61 +HOL-Proofs-ex: HOL-Proofs $(LOG)/HOL-Proofs-ex.gz
1.62 +
1.63 +$(LOG)/HOL-Proofs-ex.gz: $(OUT)/HOL-Proofs \
1.64 + Proofs/ex/ROOT.ML Proofs/ex/Hilbert_Classical.thy
1.65 + @cd Proofs; $(ISABELLE_TOOL) usedir -p 2 -q 0 $(OUT)/HOL-Proofs ex
1.66 +
1.67 +
1.68 +## HOL-Proofs-Extraction
1.69 +
1.70 +HOL-Proofs-Extraction: HOL-Proofs $(LOG)/HOL-Proofs-Extraction.gz
1.71 +
1.72 +$(LOG)/HOL-Proofs-Extraction.gz: $(OUT)/HOL-Proofs \
1.73 + Library/Efficient_Nat.thy Proofs/Extraction/Euclid.thy \
1.74 + Proofs/Extraction/Greatest_Common_Divisor.thy \
1.75 + Proofs/Extraction/Higman.thy Proofs/Extraction/Pigeonhole.thy \
1.76 + Proofs/Extraction/QuotRem.thy Proofs/Extraction/ROOT.ML \
1.77 + Proofs/Extraction/Util.thy Proofs/Extraction/Warshall.thy \
1.78 + Proofs/Extraction/document/root.tex \
1.79 + Proofs/Extraction/document/root.bib
1.80 + @cd Proofs; $(ISABELLE_TOOL) usedir -p 2 -q 0 $(OUT)/HOL-Proofs Extraction
1.81 +
1.82 +
1.83 ## HOL-Proofs-Lambda
1.84
1.85 HOL-Proofs-Lambda: HOL-Proofs $(LOG)/HOL-Proofs-Lambda.gz
1.86
1.87 -$(LOG)/HOL-Proofs-Lambda.gz: $(OUT)/HOL-Proofs Lambda/Commutation.thy \
1.88 - Lambda/Eta.thy Lambda/InductTermi.thy Lambda/Lambda.thy \
1.89 - Lambda/ListApplication.thy Lambda/ListBeta.thy Lambda/ListOrder.thy \
1.90 - Lambda/NormalForm.thy Lambda/ParRed.thy Lambda/Standardization.thy \
1.91 - Lambda/StrongNorm.thy Lambda/Type.thy Lambda/WeakNorm.thy \
1.92 - Lambda/ROOT.ML Lambda/document/root.bib Lambda/document/root.tex
1.93 - @$(ISABELLE_TOOL) usedir -g true -m no_brackets -p 2 -q 0 $(OUT)/HOL-Proofs Lambda
1.94 +$(LOG)/HOL-Proofs-Lambda.gz: $(OUT)/HOL-Proofs \
1.95 + Proofs/Lambda/Commutation.thy Proofs/Lambda/Eta.thy \
1.96 + Proofs/Lambda/InductTermi.thy Proofs/Lambda/Lambda.thy \
1.97 + Proofs/Lambda/ListApplication.thy Proofs/Lambda/ListBeta.thy \
1.98 + Proofs/Lambda/ListOrder.thy Proofs/Lambda/NormalForm.thy \
1.99 + Proofs/Lambda/ParRed.thy Proofs/Lambda/Standardization.thy \
1.100 + Proofs/Lambda/StrongNorm.thy Proofs/Lambda/Type.thy \
1.101 + Proofs/Lambda/WeakNorm.thy Proofs/Lambda/ROOT.ML \
1.102 + Proofs/Lambda/document/root.bib Proofs/Lambda/document/root.tex
1.103 + @cd Proofs; $(ISABELLE_TOOL) usedir -g true -m no_brackets -p 2 -q 0 $(OUT)/HOL-Proofs Lambda
1.104
1.105
1.106 ## HOL-Prolog
1.107 @@ -940,19 +970,6 @@
1.108 @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Bali
1.109
1.110
1.111 -## HOL-Proofs-Extraction
1.112 -
1.113 -HOL-Proofs-Extraction: HOL-Proofs $(LOG)/HOL-Proofs-Extraction.gz
1.114 -
1.115 -$(LOG)/HOL-Proofs-Extraction.gz: $(OUT)/HOL-Proofs \
1.116 - Library/Efficient_Nat.thy Extraction/Euclid.thy \
1.117 - Extraction/Greatest_Common_Divisor.thy Extraction/Higman.thy \
1.118 - Extraction/Pigeonhole.thy Extraction/QuotRem.thy Extraction/ROOT.ML \
1.119 - Extraction/Util.thy Extraction/Warshall.thy \
1.120 - Extraction/document/root.tex Extraction/document/root.bib
1.121 - @$(ISABELLE_TOOL) usedir -p 2 -q 0 $(OUT)/HOL-Proofs Extraction
1.122 -
1.123 -
1.124 ## HOL-IOA
1.125
1.126 HOL-IOA: HOL $(LOG)/HOL-IOA.gz
1.127 @@ -977,29 +994,27 @@
1.128 HOL-ex: HOL $(LOG)/HOL-ex.gz
1.129
1.130 $(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy \
1.131 - Number_Theory/Primes.thy \
1.132 - ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy \
1.133 - ex/Arithmetic_Series_Complex.thy ex/BT.thy ex/BinEx.thy \
1.134 - ex/Binary.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy \
1.135 - ex/CodegenSML_Test.thy ex/Coherent.thy ex/Dedekind_Real.thy \
1.136 - ex/Efficient_Nat_examples.thy ex/Eval_Examples.thy ex/Fundefs.thy \
1.137 - ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy \
1.138 - ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy \
1.139 - ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy \
1.140 + Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy \
1.141 + ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy ex/BT.thy \
1.142 + ex/BinEx.thy ex/Binary.thy ex/CTL.thy ex/Chinese.thy \
1.143 + ex/Classical.thy ex/CodegenSML_Test.thy ex/Coherent.thy \
1.144 + ex/Dedekind_Real.thy ex/Efficient_Nat_examples.thy \
1.145 + ex/Eval_Examples.thy ex/Fundefs.thy ex/Gauge_Integration.thy \
1.146 + ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy \
1.147 + ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \
1.148 ex/Induction_Schema.thy ex/InductiveInvariant.thy \
1.149 ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy \
1.150 - ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy \
1.151 - ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy \
1.152 - ex/Multiquote.thy ex/NatSum.thy ex/Numeral.thy ex/PER.thy \
1.153 - ex/PresburgerEx.thy ex/Primrec.thy \
1.154 - ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy \
1.155 + ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy \
1.156 + ex/Meson_Test.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy \
1.157 + ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
1.158 + ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy \
1.159 ex/ROOT.ML ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy \
1.160 ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \
1.161 ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy \
1.162 ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy ex/Tree23.thy \
1.163 - ex/Unification.thy ex/While_Combinator_Example.thy ex/document/root.bib \
1.164 - ex/document/root.tex \
1.165 - ex/set.thy ex/svc_funcs.ML ex/svc_test.thy
1.166 + ex/Unification.thy ex/While_Combinator_Example.thy \
1.167 + ex/document/root.bib ex/document/root.tex ex/set.thy ex/svc_funcs.ML \
1.168 + ex/svc_test.thy
1.169 @$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
1.170
1.171
1.172 @@ -1137,6 +1152,7 @@
1.173 Library/Nat_Bijection.thy Library/Countable.thy
1.174 @cd Probability; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Multivariate_Analysis HOL-Probability
1.175
1.176 +
1.177 ## HOL-Nominal
1.178
1.179 HOL-Nominal: HOL $(OUT)/HOL-Nominal
1.180 @@ -1160,7 +1176,7 @@
1.181
1.182 HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz
1.183
1.184 -$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal \
1.185 +$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal \
1.186 Nominal/Examples/Nominal_Examples.thy \
1.187 Nominal/Examples/CK_Machine.thy \
1.188 Nominal/Examples/CR.thy \
1.189 @@ -1352,7 +1368,8 @@
1.190 $(LOG)/HOL-Old_Number_Theory.gz $(LOG)/HOL-Plain.gz \
1.191 $(LOG)/HOL-Predicate_Compile_Examples.gz \
1.192 $(LOG)/HOL-Probability.gz $(LOG)/HOL-Prolog.gz \
1.193 - $(LOG)/HOL-Proofs.gz $(LOG)/HOL-Proofs-Extraction.gz \
1.194 + $(LOG)/HOL-Proofs.gz $(LOG)/HOL-Proofs-ex.gz \
1.195 + $(LOG)/HOL-Proofs-Extraction.gz \
1.196 $(LOG)/HOL-Proofs-Lambda.gz $(LOG)/HOL-SET_Protocol.gz \
1.197 $(LOG)/HOL-Word-SMT_Examples.gz \
1.198 $(LOG)/HOL-Statespace.gz $(LOG)/HOL-Subst.gz \