--- a/src/HOL/IsaMakefile Tue Jul 19 14:35:44 2011 +0200
+++ b/src/HOL/IsaMakefile Tue Jul 19 14:36:12 2011 +0200
@@ -450,7 +450,7 @@
Library/Continuity.thy Library/Convex.thy Library/Countable.thy \
Library/Diagonalize.thy Library/Dlist.thy Library/Dlist_Cset.thy \
Library/Efficient_Nat.thy Library/Eval_Witness.thy \
- Library/Executable_Set.thy Library/Extended_Reals.thy \
+ Library/Executable_Set.thy Library/Extended_Real.thy \
Library/Extended_Nat.thy Library/Float.thy \
Library/Formal_Power_Series.thy Library/Fraction_Field.thy \
Library/FrechetDeriv.thy Library/Cset.thy Library/FuncSet.thy \
@@ -1203,7 +1203,7 @@
Multivariate_Analysis/Topology_Euclidean_Space.thy \
Multivariate_Analysis/document/root.tex \
Multivariate_Analysis/normarith.ML Library/Glbs.thy \
- Library/Extended_Reals.thy Library/Indicator_Function.thy \
+ Library/Extended_Real.thy Library/Indicator_Function.thy \
Library/Inner_Product.thy Library/Numeral_Type.thy Library/Convex.thy \
Library/FrechetDeriv.thy Library/Product_Vector.thy \
Library/Product_plus.thy