--- a/src/HOL/Import/HOLLightReal.thy Sat Mar 03 21:00:31 2012 +0100 +++ b/src/HOL/Import/HOLLightReal.thy Sat Mar 03 21:01:23 2012 +0100 @@ -326,3 +326,4 @@ by (simp add: ext) end +