# HG changeset patch
# User berghofe
# Date 1127672233 -7200
# Node ID 409983bbaf00c729da8b38e67389265d38d17c8b
# Parent  1db9597176c8e04cb964e7c7101229c8d34f540f
Added ExecutableSet and Taylor.

diff -r 1db9597176c8 -r 409983bbaf00 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sun Sep 25 20:15:29 2005 +0200
+++ b/src/HOL/IsaMakefile	Sun Sep 25 20:17:13 2005 +0200
@@ -156,6 +156,7 @@
   Hyperreal/Ln.thy Hyperreal/MacLaurin.thy Hyperreal/NatStar.thy		\
   Hyperreal/NSA.thy Hyperreal/NthRoot.thy Hyperreal/Poly.thy			\
   Hyperreal/SEQ.thy Hyperreal/Series.thy Hyperreal/Star.thy			\
+  Hyperreal/Taylor.thy								\
   Hyperreal/Transcendental.thy Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML	\
   Complex/Complex_Main.thy Complex/CLim.thy Complex/CSeries.thy			\
   Complex/CStar.thy Complex/Complex.thy Complex/ComplexBin.thy			\
@@ -180,7 +181,8 @@
 
 $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \
   Library/SetsAndFunctions.thy Library/BigO.thy \
-  Library/EfficientNat.thy Library/FuncSet.thy Library/Library.thy \
+  Library/EfficientNat.thy Library/ExecutableSet.thy \
+  Library/FuncSet.thy Library/Library.thy \
   Library/List_Prefix.thy Library/Multiset.thy Library/NatPair.thy \
   Library/Permutation.thy Library/Primes.thy Library/Quotient.thy \
   Library/Nat_Infinity.thy Library/Word.thy Library/word_setup.ML \
@@ -484,7 +486,8 @@
 
 HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz
 
-$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL MicroJava/ROOT.ML \
+$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL Library/ExecutableSet.thy \
+  MicroJava/ROOT.ML \
   MicroJava/Comp/AuxLemmas.thy \
   MicroJava/Comp/CorrComp.thy \
   MicroJava/Comp/CorrCompTp.thy \
@@ -549,7 +552,7 @@
 
 HOL-Extraction: HOL $(LOG)/HOL-Extraction.gz
 
-$(LOG)/HOL-Extraction.gz: $(OUT)/HOL \
+$(LOG)/HOL-Extraction.gz: $(OUT)/HOL Library/EfficientNat.thy \
   Extraction/Higman.thy Extraction/ROOT.ML Extraction/Pigeonhole.thy \
   Extraction/QuotRem.thy \
   Extraction/Warshall.thy Extraction/document/root.tex \