Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
float2real is now globally available
authorobua
Fri, 03 Sep 2004 20:20:44 +0200
changeset 15180 6d3f59785197
parent 15179 b8ef323fd41e
child 15181 8d9575d1caa7
float2real is now globally available
src/HOL/Matrix/MatrixLP.ML file | annotate | diff | comparison | revisions 
--- 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)
isabelle