# HG changeset patch
# User haftmann
# Date 1379606634 -7200
# Node ID eab25a77af3952f387d7485705163f46d3209f56
# Parent  82799e03fff7f1fbacf495208abbfad546618a37
dropped dead code

diff -r 82799e03fff7 -r eab25a77af39 src/HOL/Matrix_LP/matrixlp.ML
--- a/src/HOL/Matrix_LP/matrixlp.ML	Thu Sep 19 17:38:03 2013 +0200
+++ b/src/HOL/Matrix_LP/matrixlp.ML	Thu Sep 19 18:03:54 2013 +0200
@@ -17,25 +17,6 @@
   "SparseMatrix.sorted_sp_simps"
   "ComputeNumeral.natnorm"}; (*"ComputeNumeral.number_norm"*)
 
-val spm_mult_le_dual_prts_no_let_real = @{thm "spm_mult_le_dual_prts_no_let" [where ?'a = real]}
-
-fun lp_dual_estimate_prt lptfile prec =
-  let
-    val cert = cterm_of @{theory}
-    fun var s x = (cert (Var ((s, 0), FloatSparseMatrixBuilder.spmatT)), x)
-    val l = Fspmlp.load lptfile prec false
-    val (y, (A1, A2), (c1, c2), b, (r1, r2)) =
-      let
-        open Fspmlp
-      in
-        (y l |> cert, A l |> pairself cert, c l |> pairself cert, b l |> cert, r12 l |> pairself cert)
-      end
-  in
-    Thm.instantiate ([],
-      [var "A1" A1, var "A2" A2, var "y" y, var "c1" c1, var "c2" c2, var "r1" r1, var "r2" r2, var "b" b])
-      spm_mult_le_dual_prts_no_let_real
-  end
-
 val computer = PCompute.make Compute.SML @{theory} compute_thms []
 
 fun matrix_compute c = hd (PCompute.rewrite computer [c])
@@ -49,6 +30,4 @@
     removeTrue th
   end
 
-val prove_bound = matrix_simplify oo lp_dual_estimate_prt;
-
 end