--- a/src/HOL/IsaMakefile Tue Sep 07 11:51:53 2010 +0200
+++ b/src/HOL/IsaMakefile Tue Sep 07 11:52:43 2010 +0200
@@ -57,6 +57,7 @@
HOL-Quotient_Examples \
HOL-Predicate_Compile_Examples \
HOL-Prolog \
+ HOL-Proofs-ex \
HOL-Proofs-Extraction \
HOL-Proofs-Lambda \
HOL-SET_Protocol \
@@ -92,8 +93,6 @@
HOL-Main: Pure $(OUT)/HOL-Main
-HOL-Proofs: Pure $(OUT)/HOL-Proofs
-
Pure:
@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
@@ -145,7 +144,7 @@
$(OUT)/HOL-Base: base.ML $(BASE_DEPENDENCIES)
@$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base
-PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES)\
+PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES) \
Complete_Lattice.thy \
Datatype.thy \
Extraction.thy \
@@ -357,9 +356,6 @@
$(OUT)/HOL-Main: main.ML $(MAIN_DEPENDENCIES)
@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
-$(OUT)/HOL-Proofs: main.ML $(MAIN_DEPENDENCIES)
- @$(ISABELLE_TOOL) usedir -b -f main.ML -g true -p 2 -q 0 $(OUT)/Pure HOL-Proofs
-
HOL_DEPENDENCIES = $(MAIN_DEPENDENCIES) \
Archimedean_Field.thy \
Complex.thy \
@@ -392,7 +388,6 @@
@$(ISABELLE_TOOL) usedir -b -g true $(OUT)/Pure HOL
-
## HOL-Library
HOL-Library: HOL $(OUT)/HOL-Library
@@ -787,7 +782,7 @@
$(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/Nested_Environment.thy \
Library/List_Prefix.thy Unix/ROOT.ML Unix/Unix.thy \
Unix/document/root.bib Unix/document/root.tex
- @$(ISABELLE_TOOL) usedir $(OUT)/HOL Unix
+ @$(ISABELLE_TOOL) usedir -m no_brackets -m no_type_brackets $(OUT)/HOL Unix
## HOL-ZF
@@ -857,17 +852,52 @@
@$(ISABELLE_TOOL) usedir -D generated $(OUT)/HOL Docs
+## HOL-Proofs
+
+HOL-Proofs: Pure $(OUT)/HOL-Proofs
+
+$(OUT)/HOL-Proofs: main.ML $(MAIN_DEPENDENCIES)
+ @$(ISABELLE_TOOL) usedir -b -f main.ML -g true -p 2 -q 0 $(OUT)/Pure HOL-Proofs
+
+
+## HOL-Proofs-ex
+
+HOL-Proofs-ex: HOL-Proofs $(LOG)/HOL-Proofs-ex.gz
+
+$(LOG)/HOL-Proofs-ex.gz: $(OUT)/HOL-Proofs \
+ Proofs/ex/ROOT.ML Proofs/ex/Hilbert_Classical.thy
+ @cd Proofs; $(ISABELLE_TOOL) usedir -p 2 -q 0 $(OUT)/HOL-Proofs ex
+
+
+## HOL-Proofs-Extraction
+
+HOL-Proofs-Extraction: HOL-Proofs $(LOG)/HOL-Proofs-Extraction.gz
+
+$(LOG)/HOL-Proofs-Extraction.gz: $(OUT)/HOL-Proofs \
+ Library/Efficient_Nat.thy Proofs/Extraction/Euclid.thy \
+ Proofs/Extraction/Greatest_Common_Divisor.thy \
+ Proofs/Extraction/Higman.thy Proofs/Extraction/Pigeonhole.thy \
+ Proofs/Extraction/QuotRem.thy Proofs/Extraction/ROOT.ML \
+ Proofs/Extraction/Util.thy Proofs/Extraction/Warshall.thy \
+ Proofs/Extraction/document/root.tex \
+ Proofs/Extraction/document/root.bib
+ @cd Proofs; $(ISABELLE_TOOL) usedir -p 2 -q 0 $(OUT)/HOL-Proofs Extraction
+
+
## HOL-Proofs-Lambda
HOL-Proofs-Lambda: HOL-Proofs $(LOG)/HOL-Proofs-Lambda.gz
-$(LOG)/HOL-Proofs-Lambda.gz: $(OUT)/HOL-Proofs Lambda/Commutation.thy \
- Lambda/Eta.thy Lambda/InductTermi.thy Lambda/Lambda.thy \
- Lambda/ListApplication.thy Lambda/ListBeta.thy Lambda/ListOrder.thy \
- Lambda/NormalForm.thy Lambda/ParRed.thy Lambda/Standardization.thy \
- Lambda/StrongNorm.thy Lambda/Type.thy Lambda/WeakNorm.thy \
- Lambda/ROOT.ML Lambda/document/root.bib Lambda/document/root.tex
- @$(ISABELLE_TOOL) usedir -g true -m no_brackets -p 2 -q 0 $(OUT)/HOL-Proofs Lambda
+$(LOG)/HOL-Proofs-Lambda.gz: $(OUT)/HOL-Proofs \
+ Proofs/Lambda/Commutation.thy Proofs/Lambda/Eta.thy \
+ Proofs/Lambda/InductTermi.thy Proofs/Lambda/Lambda.thy \
+ Proofs/Lambda/ListApplication.thy Proofs/Lambda/ListBeta.thy \
+ Proofs/Lambda/ListOrder.thy Proofs/Lambda/NormalForm.thy \
+ Proofs/Lambda/ParRed.thy Proofs/Lambda/Standardization.thy \
+ Proofs/Lambda/StrongNorm.thy Proofs/Lambda/Type.thy \
+ Proofs/Lambda/WeakNorm.thy Proofs/Lambda/ROOT.ML \
+ Proofs/Lambda/document/root.bib Proofs/Lambda/document/root.tex
+ @cd Proofs; $(ISABELLE_TOOL) usedir -g true -m no_brackets -p 2 -q 0 $(OUT)/HOL-Proofs Lambda
## HOL-Prolog
@@ -942,19 +972,6 @@
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Bali
-## HOL-Proofs-Extraction
-
-HOL-Proofs-Extraction: HOL-Proofs $(LOG)/HOL-Proofs-Extraction.gz
-
-$(LOG)/HOL-Proofs-Extraction.gz: $(OUT)/HOL-Proofs \
- Library/Efficient_Nat.thy Extraction/Euclid.thy \
- Extraction/Greatest_Common_Divisor.thy Extraction/Higman.thy \
- Extraction/Pigeonhole.thy Extraction/QuotRem.thy Extraction/ROOT.ML \
- Extraction/Util.thy Extraction/Warshall.thy \
- Extraction/document/root.tex Extraction/document/root.bib
- @$(ISABELLE_TOOL) usedir -p 2 -q 0 $(OUT)/HOL-Proofs Extraction
-
-
## HOL-IOA
HOL-IOA: HOL $(LOG)/HOL-IOA.gz
@@ -979,29 +996,27 @@
HOL-ex: HOL $(LOG)/HOL-ex.gz
$(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy \
- Number_Theory/Primes.thy \
- ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy \
- ex/Arithmetic_Series_Complex.thy ex/BT.thy ex/BinEx.thy \
- ex/Binary.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy \
- ex/CodegenSML_Test.thy ex/Coherent.thy ex/Dedekind_Real.thy \
- ex/Efficient_Nat_examples.thy ex/Eval_Examples.thy ex/Fundefs.thy \
- ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy \
- ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy \
- ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy \
+ Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy \
+ ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy ex/BT.thy \
+ ex/BinEx.thy ex/Binary.thy ex/CTL.thy ex/Chinese.thy \
+ ex/Classical.thy ex/CodegenSML_Test.thy ex/Coherent.thy \
+ ex/Dedekind_Real.thy ex/Efficient_Nat_examples.thy \
+ ex/Eval_Examples.thy ex/Fundefs.thy ex/Gauge_Integration.thy \
+ ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy \
+ ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \
ex/Induction_Schema.thy ex/InductiveInvariant.thy \
ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy \
- ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy \
- ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy \
- ex/Multiquote.thy ex/NatSum.thy ex/Numeral.thy ex/PER.thy \
- ex/PresburgerEx.thy ex/Primrec.thy \
- ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy \
+ ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy \
+ ex/Meson_Test.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy \
+ ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
+ ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy \
ex/ROOT.ML ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy \
ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \
ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy \
ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy ex/Tree23.thy \
- ex/Unification.thy ex/While_Combinator_Example.thy ex/document/root.bib \
- ex/document/root.tex \
- ex/set.thy ex/svc_funcs.ML ex/svc_test.thy
+ ex/Unification.thy ex/While_Combinator_Example.thy \
+ ex/document/root.bib ex/document/root.tex ex/set.thy ex/svc_funcs.ML \
+ ex/svc_test.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
@@ -1139,6 +1154,7 @@
Library/Nat_Bijection.thy Library/Countable.thy
@cd Probability; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Multivariate_Analysis HOL-Probability
+
## HOL-Nominal
HOL-Nominal: HOL $(OUT)/HOL-Nominal
@@ -1162,7 +1178,7 @@
HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz
-$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal \
+$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal \
Nominal/Examples/Nominal_Examples.thy \
Nominal/Examples/CK_Machine.thy \
Nominal/Examples/CR.thy \
@@ -1361,7 +1377,8 @@
$(LOG)/HOL-Old_Number_Theory.gz $(LOG)/HOL-Plain.gz \
$(LOG)/HOL-Predicate_Compile_Examples.gz \
$(LOG)/HOL-Probability.gz $(LOG)/HOL-Prolog.gz \
- $(LOG)/HOL-Proofs.gz $(LOG)/HOL-Proofs-Extraction.gz \
+ $(LOG)/HOL-Proofs.gz $(LOG)/HOL-Proofs-ex.gz \
+ $(LOG)/HOL-Proofs-Extraction.gz \
$(LOG)/HOL-Proofs-Lambda.gz $(LOG)/HOL-SET_Protocol.gz \
$(LOG)/HOL-Word-SMT_Examples.gz \
$(LOG)/HOL-Statespace.gz $(LOG)/HOL-Subst.gz \