diff -r 8885ba629692 -r 15927c040731 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Mar 14 14:37:37 2011 +0100
+++ b/src/HOL/IsaMakefile	Mon Mar 14 14:37:39 2011 +0100
@@ -437,10 +437,10 @@
   Library/ContNotDenum.thy Library/Continuity.thy Library/Convex.thy	\
   Library/Countable.thy Library/Diagonalize.thy Library/Dlist.thy	\
   Library/Efficient_Nat.thy Library/Eval_Witness.thy 			\
-  Library/Executable_Set.thy Library/Float.thy				\
-  Library/Formal_Power_Series.thy Library/Fraction_Field.thy		\
-  Library/FrechetDeriv.thy Library/Cset.thy Library/FuncSet.thy		\
-  Library/Function_Algebras.thy						\
+  Library/Executable_Set.thy Library/Extended_Reals.thy			\
+  Library/Float.thy Library/Formal_Power_Series.thy			\
+  Library/Fraction_Field.thy Library/FrechetDeriv.thy Library/Cset.thy	\
+  Library/FuncSet.thy Library/Function_Algebras.thy			\
   Library/Fundamental_Theorem_Algebra.thy Library/Glbs.thy		\
   Library/Indicator_Function.thy Library/Infinite_Set.thy		\
   Library/Inner_Product.thy Library/Kleene_Algebra.thy			\