1.1 --- a/src/HOL/Matrix_LP/matrixlp.ML	Thu Sep 19 17:38:03 2013 +0200
     1.2 +++ b/src/HOL/Matrix_LP/matrixlp.ML	Thu Sep 19 18:03:54 2013 +0200
     1.3 @@ -17,25 +17,6 @@
     1.4    "SparseMatrix.sorted_sp_simps"
     1.5    "ComputeNumeral.natnorm"}; (*"ComputeNumeral.number_norm"*)
     1.6  
     1.7 -val spm_mult_le_dual_prts_no_let_real = @{thm "spm_mult_le_dual_prts_no_let" [where ?'a = real]}
     1.8 -
     1.9 -fun lp_dual_estimate_prt lptfile prec =
    1.10 -  let
    1.11 -    val cert = cterm_of @{theory}
    1.12 -    fun var s x = (cert (Var ((s, 0), FloatSparseMatrixBuilder.spmatT)), x)
    1.13 -    val l = Fspmlp.load lptfile prec false
    1.14 -    val (y, (A1, A2), (c1, c2), b, (r1, r2)) =
    1.15 -      let
    1.16 -        open Fspmlp
    1.17 -      in
    1.18 -        (y l |> cert, A l |> pairself cert, c l |> pairself cert, b l |> cert, r12 l |> pairself cert)
    1.19 -      end
    1.20 -  in
    1.21 -    Thm.instantiate ([],
    1.22 -      [var "A1" A1, var "A2" A2, var "y" y, var "c1" c1, var "c2" c2, var "r1" r1, var "r2" r2, var "b" b])
    1.23 -      spm_mult_le_dual_prts_no_let_real
    1.24 -  end
    1.25 -
    1.26  val computer = PCompute.make Compute.SML @{theory} compute_thms []
    1.27  
    1.28  fun matrix_compute c = hd (PCompute.rewrite computer [c])
    1.29 @@ -49,6 +30,4 @@
    1.30      removeTrue th
    1.31    end
    1.32  
    1.33 -val prove_bound = matrix_simplify oo lp_dual_estimate_prt;
    1.34 -
    1.35  end