author | obua |
Fri, 03 Sep 2004 20:20:44 +0200 | |
changeset 15180 | 6d3f59785197 |
parent 15179 | b8ef323fd41e |
child 15181 | 8d9575d1caa7 |
1.1 --- a/src/HOL/Matrix/MatrixLP.ML Fri Sep 03 17:46:47 2004 +0200 1.2 +++ b/src/HOL/Matrix/MatrixLP.ML Fri Sep 03 20:20:44 2004 +0200 1.3 @@ -73,10 +73,10 @@ 1.4 removeTrue th 1.5 end 1.6 1.7 +end 1.8 + 1.9 fun float2real (x,y) = (Real.fromInt x) * (Math.pow (2.0, Real.fromInt y)) 1.10 1.11 -end 1.12 - 1.13 val result = ref ([]:thm list) 1.14 1.15 fun run c = timeit (fn () => (result := [MatrixLP.simplify c]; ()))