1.1 --- a/src/HOL/IsaMakefile Thu Jul 08 16:17:44 2010 +0200
1.2 +++ b/src/HOL/IsaMakefile Thu Jul 08 16:17:44 2010 +0200
1.3 @@ -531,7 +531,7 @@
1.4
1.5 HOL-Generate-HOLLight: HOL $(LOG)/HOL-Generate-HOLLight.gz
1.6
1.7 -$(LOG)/HOL-Generate-HOLLight.gz: $(OUT)/HOL \
1.8 +$(LOG)/HOL-Generate-HOLLight.gz: $(OUT)/HOL \
1.9 $(IMPORTER_HOLLIGHT_FILES) Import/Generate-HOLLight/GenHOLLight.thy \
1.10 Import/Generate-HOLLight/ROOT.ML
1.11 @cd Import; $(ISABELLE_TOOL) usedir $(OUT)/HOL Generate-HOLLight
1.12 @@ -552,7 +552,7 @@
1.13 seq.imp state_transformer.imp sum.imp topology.imp transc.imp word32.imp \
1.14 word_base.imp word_bitop.imp word_num.imp
1.15
1.16 -$(LOG)/HOL4.gz: $(OUT)/HOL $(IMPORTER_FILES) \
1.17 +$(LOG)/HOL4.gz: $(OUT)/HOL $(IMPORTER_FILES) \
1.18 $(HOL_IMPORT_FILES:%=Import/HOL/%) Import/HOL/HOL4Base.thy \
1.19 Import/HOL/HOL4Prob.thy Import/HOL/HOL4Real.thy \
1.20 Import/HOL/HOL4Vec.thy Import/HOL/HOL4Word32.thy Import/HOL/HOL4.thy \
1.21 @@ -561,7 +561,7 @@
1.22
1.23 HOLLight: HOL $(LOG)/HOLLight.gz
1.24
1.25 -$(LOG)/HOLLight.gz: $(OUT)/HOL $(IMPORTER_HOLLIGHT_FILES) \
1.26 +$(LOG)/HOLLight.gz: $(OUT)/HOL $(IMPORTER_HOLLIGHT_FILES) \
1.27 Import/HOLLight/hollight.imp Import/HOLLight/HOLLight.thy \
1.28 Import/HOLLight/ROOT.ML
1.29 @cd Import/HOLLight; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOLLight
1.30 @@ -639,7 +639,8 @@
1.31 HOL-Codegenerator_Test: HOL-Library $(LOG)/HOL-Codegenerator_Test.gz
1.32
1.33 $(LOG)/HOL-Codegenerator_Test.gz: $(OUT)/HOL-Library \
1.34 - Codegenerator_Test/ROOT.ML Codegenerator_Test/Candidates.thy \
1.35 + Codegenerator_Test/ROOT.ML \
1.36 + Codegenerator_Test/Candidates.thy \
1.37 Codegenerator_Test/Candidates_Pretty.thy \
1.38 Codegenerator_Test/Generate.thy \
1.39 Codegenerator_Test/Generate_Pretty.thy
1.40 @@ -650,10 +651,10 @@
1.41
1.42 HOL-Metis_Examples: HOL $(LOG)/HOL-Metis_Examples.gz
1.43
1.44 -$(LOG)/HOL-Metis_Examples.gz: $(OUT)/HOL Metis_Examples/ROOT.ML \
1.45 - Metis_Examples/Abstraction.thy Metis_Examples/BigO.thy \
1.46 - Metis_Examples/BT.thy Metis_Examples/Message.thy \
1.47 - Metis_Examples/Tarski.thy Metis_Examples/TransClosure.thy \
1.48 +$(LOG)/HOL-Metis_Examples.gz: $(OUT)/HOL Metis_Examples/ROOT.ML \
1.49 + Metis_Examples/Abstraction.thy Metis_Examples/BigO.thy \
1.50 + Metis_Examples/BT.thy Metis_Examples/Message.thy \
1.51 + Metis_Examples/Tarski.thy Metis_Examples/TransClosure.thy \
1.52 Metis_Examples/set.thy
1.53 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Metis_Examples
1.54
1.55 @@ -778,8 +779,8 @@
1.56
1.57 HOL-Unix: HOL $(LOG)/HOL-Unix.gz
1.58
1.59 -$(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/Nested_Environment.thy \
1.60 - Library/List_Prefix.thy Unix/ROOT.ML Unix/Unix.thy \
1.61 +$(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/Nested_Environment.thy \
1.62 + Library/List_Prefix.thy Unix/ROOT.ML Unix/Unix.thy \
1.63 Unix/document/root.bib Unix/document/root.tex
1.64 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Unix
1.65
1.66 @@ -797,10 +798,10 @@
1.67
1.68 HOL-Modelcheck: HOL $(LOG)/HOL-Modelcheck.gz
1.69
1.70 -$(LOG)/HOL-Modelcheck.gz: $(OUT)/HOL Modelcheck/CTL.thy \
1.71 - Modelcheck/EindhovenExample.thy Modelcheck/EindhovenSyn.thy \
1.72 - Modelcheck/MuCalculus.thy Modelcheck/MuckeExample1.thy \
1.73 - Modelcheck/MuckeExample2.thy Modelcheck/MuckeSyn.thy \
1.74 +$(LOG)/HOL-Modelcheck.gz: $(OUT)/HOL Modelcheck/CTL.thy \
1.75 + Modelcheck/EindhovenExample.thy Modelcheck/EindhovenSyn.thy \
1.76 + Modelcheck/MuCalculus.thy Modelcheck/MuckeExample1.thy \
1.77 + Modelcheck/MuckeExample2.thy Modelcheck/MuckeSyn.thy \
1.78 Modelcheck/ROOT.ML Modelcheck/mucke_oracle.ML
1.79 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Modelcheck
1.80
1.81 @@ -859,7 +860,7 @@
1.82
1.83 HOL-Docs: HOL $(LOG)/HOL-Docs.gz
1.84
1.85 -$(LOG)/HOL-Docs.gz: $(OUT)/HOL Docs/Main_Doc.thy Docs/ROOT.ML \
1.86 +$(LOG)/HOL-Docs.gz: $(OUT)/HOL Docs/Main_Doc.thy Docs/ROOT.ML \
1.87 Docs/document/root.tex
1.88 @$(ISABELLE_TOOL) usedir -D generated $(OUT)/HOL Docs
1.89
1.90 @@ -1124,8 +1125,8 @@
1.91 Multivariate_Analysis/Real_Integration.thy \
1.92 Multivariate_Analysis/Topology_Euclidean_Space.thy \
1.93 Multivariate_Analysis/document/root.tex \
1.94 - Multivariate_Analysis/normarith.ML Library/Glbs.thy \
1.95 - Library/Inner_Product.thy Library/Numeral_Type.thy \
1.96 + Multivariate_Analysis/normarith.ML Library/Glbs.thy \
1.97 + Library/Inner_Product.thy Library/Numeral_Type.thy \
1.98 Library/Convex.thy Library/FrechetDeriv.thy \
1.99 Library/Product_Vector.thy Library/Product_plus.thy
1.100 @cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Multivariate_Analysis
1.101 @@ -1135,15 +1136,15 @@
1.102
1.103 HOL-Probability: HOL $(OUT)/HOL-Probability
1.104
1.105 -$(OUT)/HOL-Probability: $(OUT)/HOL Probability/ROOT.ML \
1.106 - Probability/Probability.thy Probability/Sigma_Algebra.thy \
1.107 - Probability/SeriesPlus.thy Probability/Caratheodory.thy \
1.108 - Probability/Borel.thy Probability/Measure.thy \
1.109 - Probability/Lebesgue.thy Probability/Product_Measure.thy \
1.110 - Probability/Probability_Space.thy Probability/Information.thy \
1.111 - Probability/ex/Dining_Cryptographers.thy Library/FuncSet.thy \
1.112 - Library/Convex.thy Library/Product_Vector.thy \
1.113 - Library/Product_plus.thy Library/Inner_Product.thy \
1.114 +$(OUT)/HOL-Probability: $(OUT)/HOL Probability/ROOT.ML \
1.115 + Probability/Probability.thy Probability/Sigma_Algebra.thy \
1.116 + Probability/SeriesPlus.thy Probability/Caratheodory.thy \
1.117 + Probability/Borel.thy Probability/Measure.thy \
1.118 + Probability/Lebesgue.thy Probability/Product_Measure.thy \
1.119 + Probability/Probability_Space.thy Probability/Information.thy \
1.120 + Probability/ex/Dining_Cryptographers.thy Library/FuncSet.thy \
1.121 + Library/Convex.thy Library/Product_Vector.thy \
1.122 + Library/Product_plus.thy Library/Inner_Product.thy \
1.123 Library/Nat_Bijection.thy
1.124 @cd Probability; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Probability
1.125
1.126 @@ -1252,7 +1253,7 @@
1.127
1.128 HOL-NSA-Examples: HOL-NSA $(LOG)/HOL-NSA-Examples.gz
1.129
1.130 -$(LOG)/HOL-NSA-Examples.gz: $(OUT)/HOL-NSA NSA/Examples/ROOT.ML \
1.131 +$(LOG)/HOL-NSA-Examples.gz: $(OUT)/HOL-NSA NSA/Examples/ROOT.ML \
1.132 NSA/Examples/NSPrimes.thy
1.133 @cd NSA; $(ISABELLE_TOOL) usedir $(OUT)/HOL-NSA Examples
1.134
1.135 @@ -1320,7 +1321,7 @@
1.136 HOL-Quotient_Examples: HOL $(LOG)/HOL-Quotient_Examples.gz
1.137
1.138 $(LOG)/HOL-Quotient_Examples.gz: $(OUT)/HOL \
1.139 - Quotient_Examples/FSet.thy Quotient_Examples/Quotient_Int.thy \
1.140 + Quotient_Examples/FSet.thy Quotient_Examples/Quotient_Int.thy \
1.141 Quotient_Examples/Quotient_Message.thy
1.142 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples
1.143