# HG changeset patch
# User wenzelm
# Date 1368556330 -7200
# Node ID 700693cb96f13830c3030210315b26970647015f
# Parent  a9725750c53a733f063a8e0d88e2367d96644bd5
removed dead code;

diff -r a9725750c53a -r 700693cb96f1 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