--- a/src/HOL/IsaMakefile Mon Dec 29 13:23:53 2008 +0100
+++ b/src/HOL/IsaMakefile Mon Dec 29 14:08:08 2008 +0100
@@ -261,7 +261,7 @@
$(OUT)/HOL: ROOT.ML $(MAIN_DEPENDENCIES) \
Complex_Main.thy \
Complex.thy \
- Complex/Fundamental_Theorem_Algebra.thy \
+ Fundamental_Theorem_Algebra.thy \
Deriv.thy \
Fact.thy \
FrechetDeriv.thy \
@@ -271,11 +271,11 @@
Log.thy \
MacLaurin.thy \
NthRoot.thy \
- Hyperreal/SEQ.thy \
+ SEQ.thy \
Series.thy \
Taylor.thy \
Transcendental.thy \
- Library/Dense_Linear_Order.thy \
+ Dense_Linear_Order.thy \
GCD.thy \
Order_Relation.thy \
Parity.thy \
@@ -287,7 +287,7 @@
RealDef.thy \
RealPow.thy \
Real.thy \
- Real/RealVector.thy \
+ RealVector.thy \
Tools/float_syntax.ML \
Tools/rat_arith.ML \
Tools/real_arith.ML \
@@ -337,16 +337,16 @@
HOL-HahnBanach: HOL $(LOG)/HOL-HahnBanach.gz
$(LOG)/HOL-HahnBanach.gz: $(OUT)/HOL \
- Real/HahnBanach/Bounds.thy Real/HahnBanach/FunctionNorm.thy \
- Real/HahnBanach/FunctionOrder.thy Real/HahnBanach/HahnBanach.thy \
- Real/HahnBanach/HahnBanachExtLemmas.thy \
- Real/HahnBanach/HahnBanachSupLemmas.thy \
- Real/HahnBanach/Linearform.thy Real/HahnBanach/NormedSpace.thy \
- Real/HahnBanach/README.html Real/HahnBanach/ROOT.ML \
- Real/HahnBanach/Subspace.thy Real/HahnBanach/VectorSpace.thy \
- Real/HahnBanach/ZornLemma.thy Real/HahnBanach/document/root.bib \
- Real/HahnBanach/document/root.tex
- @cd Real; $(ISABELLE_TOOL) usedir -g true $(OUT)/HOL HahnBanach
+ HahnBanach/Bounds.thy HahnBanach/FunctionNorm.thy \
+ HahnBanach/FunctionOrder.thy HahnBanach/HahnBanach.thy \
+ HahnBanach/HahnBanachExtLemmas.thy \
+ HahnBanach/HahnBanachSupLemmas.thy \
+ HahnBanach/Linearform.thy HahnBanach/NormedSpace.thy \
+ HahnBanach/README.html HahnBanach/ROOT.ML \
+ HahnBanach/Subspace.thy HahnBanach/VectorSpace.thy \
+ HahnBanach/ZornLemma.thy HahnBanach/document/root.bib \
+ HahnBanach/document/root.tex
+ @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL HahnBanach
## HOL-Subst