removed dead code;
authorwenzelm
Tue May 14 20:32:10 2013 +0200 (2013-05-14)
changeset 51989700693cb96f1
parent 51988 a9725750c53a
child 51990 cc66addbba6d
removed dead code;
src/HOL/Matrix_LP/matrixlp.ML
     1.1 --- a/src/HOL/Matrix_LP/matrixlp.ML	Tue May 14 19:48:31 2013 +0200
     1.2 +++ b/src/HOL/Matrix_LP/matrixlp.ML	Tue May 14 20:32:10 2013 +0200
     1.3 @@ -6,8 +6,6 @@
     1.4  sig
     1.5    val matrix_compute : cterm -> thm
     1.6    val matrix_simplify : thm -> thm
     1.7 -  val prove_bound : string -> int -> thm
     1.8 -  val float2real : string * string -> Real.real
     1.9  end
    1.10  
    1.11  structure MatrixLP : MATRIX_LP =
    1.12 @@ -53,7 +51,4 @@
    1.13  
    1.14  val prove_bound = matrix_simplify oo lp_dual_estimate_prt;
    1.15  
    1.16 -val realFromStr = the o Real.fromString;
    1.17 -fun float2real (x, y) = realFromStr x * Math.pow (2.0, realFromStr y);
    1.18 -
    1.19  end