Added ExecutableSet and Taylor.
authorberghofe
Sun Sep 25 20:17:13 2005 +0200 (2005-09-25)
changeset 17637409983bbaf00
parent 17636 1db9597176c8
child 17638 6de497c99e4c
Added ExecutableSet and Taylor.
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/IsaMakefile	Sun Sep 25 20:15:29 2005 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Sun Sep 25 20:17:13 2005 +0200
     1.3 @@ -156,6 +156,7 @@
     1.4    Hyperreal/Ln.thy Hyperreal/MacLaurin.thy Hyperreal/NatStar.thy		\
     1.5    Hyperreal/NSA.thy Hyperreal/NthRoot.thy Hyperreal/Poly.thy			\
     1.6    Hyperreal/SEQ.thy Hyperreal/Series.thy Hyperreal/Star.thy			\
     1.7 +  Hyperreal/Taylor.thy								\
     1.8    Hyperreal/Transcendental.thy Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML	\
     1.9    Complex/Complex_Main.thy Complex/CLim.thy Complex/CSeries.thy			\
    1.10    Complex/CStar.thy Complex/Complex.thy Complex/ComplexBin.thy			\
    1.11 @@ -180,7 +181,8 @@
    1.12  
    1.13  $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \
    1.14    Library/SetsAndFunctions.thy Library/BigO.thy \
    1.15 -  Library/EfficientNat.thy Library/FuncSet.thy Library/Library.thy \
    1.16 +  Library/EfficientNat.thy Library/ExecutableSet.thy \
    1.17 +  Library/FuncSet.thy Library/Library.thy \
    1.18    Library/List_Prefix.thy Library/Multiset.thy Library/NatPair.thy \
    1.19    Library/Permutation.thy Library/Primes.thy Library/Quotient.thy \
    1.20    Library/Nat_Infinity.thy Library/Word.thy Library/word_setup.ML \
    1.21 @@ -484,7 +486,8 @@
    1.22  
    1.23  HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz
    1.24  
    1.25 -$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL MicroJava/ROOT.ML \
    1.26 +$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL Library/ExecutableSet.thy \
    1.27 +  MicroJava/ROOT.ML \
    1.28    MicroJava/Comp/AuxLemmas.thy \
    1.29    MicroJava/Comp/CorrComp.thy \
    1.30    MicroJava/Comp/CorrCompTp.thy \
    1.31 @@ -549,7 +552,7 @@
    1.32  
    1.33  HOL-Extraction: HOL $(LOG)/HOL-Extraction.gz
    1.34  
    1.35 -$(LOG)/HOL-Extraction.gz: $(OUT)/HOL \
    1.36 +$(LOG)/HOL-Extraction.gz: $(OUT)/HOL Library/EfficientNat.thy \
    1.37    Extraction/Higman.thy Extraction/ROOT.ML Extraction/Pigeonhole.thy \
    1.38    Extraction/QuotRem.thy \
    1.39    Extraction/Warshall.thy Extraction/document/root.tex \