src/HOL/IsaMakefile

 	@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
 
 $(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 \
   Integration.thy \
   Lim.thy \
   Ln.thy \
   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 \
   Univ_Poly.thy \
   Lubs.thy \

   Rational.thy \
   RComplete.thy \
   RealDef.thy \
   RealPow.thy \
   Real.thy \
-  Real/RealVector.thy \
+  RealVector.thy \
   Tools/float_syntax.ML \
   Tools/rat_arith.ML \
   Tools/real_arith.ML \
   Tools/Qelim/ferrante_rackoff_data.ML \
   Tools/Qelim/ferrante_rackoff.ML \

 ## HOL-HahnBanach
 
 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
 
 HOL-Subst: HOL $(LOG)/HOL-Subst.gz