# HG changeset patch
# User obua
# Date 1094235644 -7200
# Node ID 6d3f59785197f19389f843e33f7be7b96000b378
# Parent  b8ef323fd41eab2fa3a570ef75821e9927222cd5
float2real is now globally available

diff -r b8ef323fd41e -r 6d3f59785197 src/HOL/Matrix/MatrixLP.ML
--- a/src/HOL/Matrix/MatrixLP.ML	Fri Sep 03 17:46:47 2004 +0200
+++ b/src/HOL/Matrix/MatrixLP.ML	Fri Sep 03 20:20:44 2004 +0200
@@ -73,9 +73,9 @@
 	removeTrue th
     end
 
-fun float2real (x,y) = (Real.fromInt x) * (Math.pow (2.0, Real.fromInt y))
+end
 
-end
+fun float2real (x,y) = (Real.fromInt x) * (Math.pow (2.0, Real.fromInt y))
 
 val result = ref ([]:thm list)