removed dead code;
authorwenzelm
Tue, 14 May 2013 20:32:10 +0200
changeset 51989 700693cb96f1
parent 51988 a9725750c53a
child 51990 cc66addbba6d
removed dead code;
src/HOL/Matrix_LP/matrixlp.ML
--- 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