--- a/src/HOL/Matrix_LP/matrixlp.ML Tue May 14 19:48:31 2013 +0200
+++ b/src/HOL/Matrix_LP/matrixlp.ML Tue May 14 20:32:10 2013 +0200
@@ -6,8 +6,6 @@
sig
val matrix_compute : cterm -> thm
val matrix_simplify : thm -> thm
- val prove_bound : string -> int -> thm
- val float2real : string * string -> Real.real
end
structure MatrixLP : MATRIX_LP =
@@ -53,7 +51,4 @@
val prove_bound = matrix_simplify oo lp_dual_estimate_prt;
-val realFromStr = the o Real.fromString;
-fun float2real (x, y) = realFromStr x * Math.pow (2.0, realFromStr y);
-
end