src/HOL/Matrix/cplex/matrixlp.ML
author wenzelm
Fri, 29 Sep 2006 22:47:51 +0200
changeset 20787 406d990006af
child 22964 2284e0d02e7f
permissions -rw-r--r--
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
20787
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/Matrix/cplex/MatrixLP.ML
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
     3
    Author:     Steven Obua
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
     4
*)
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
     5
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
     6
signature MATRIX_LP =
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
     7
sig
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
     8
  val lp_dual_estimate_prt : string -> int -> thm
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
     9
  val lp_dual_estimate_prt_primitive :
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    10
    cterm * (cterm * cterm) * (cterm * cterm) * cterm * (cterm * cterm) -> thm
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    11
  val matrix_compute : cterm -> thm
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    12
  val matrix_simplify : thm -> thm
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    13
  val prove_bound : string -> int -> thm
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    14
  val float2real : string * string -> Real.real
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    15
end
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    16
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    17
structure MatrixLP : MATRIX_LP =
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    18
struct
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    19
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    20
fun inst_real thm =
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    21
  let val certT = ctyp_of (Thm.theory_of_thm thm) in
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    22
    standard (Thm.instantiate
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    23
      ([(certT (TVar (hd (term_tvars (prop_of thm)))), certT HOLogic.realT)], []) thm)
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    24
  end
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    25
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    26
val spm_mult_le_dual_prts_no_let = thm "SparseMatrix.spm_mult_le_dual_prts_no_let"
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    27
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    28
fun lp_dual_estimate_prt_primitive (y, (A1, A2), (c1, c2), b, (r1, r2)) =
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    29
  let
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    30
    val cert = cterm_of (Thm.theory_of_thm spm_mult_le_dual_prts_no_let)
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    31
    val th = inst_real spm_mult_le_dual_prts_no_let
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    32
    fun var s x = (cert (Var ((s,0), FloatSparseMatrixBuilder.real_spmatT)), x)
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    33
    val th = Thm.instantiate ([], [var "A1" A1, var "A2" A2, var "y" y, var "c1" c1, var "c2" c2,
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    34
                                   var "r1" r1, var "r2" r2, var "b" b]) th
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    35
  in th end
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    36
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    37
fun lp_dual_estimate_prt lptfile prec =
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    38
    let
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    39
        val certificate =
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    40
            let
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    41
                open fspmlp
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    42
                val l = load lptfile prec false
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    43
            in
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    44
                (y l, A l, c l, b l, r12 l)
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    45
            end
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    46
    in
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    47
        lp_dual_estimate_prt_primitive certificate
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    48
    end
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    49
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    50
fun is_meta_eq th =
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    51
    let
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    52
        fun check ((Const ("==", _)) $ _ $ _) = true
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    53
          | check _ = false
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    54
    in
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    55
        check (concl_of th)
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    56
    end
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    57
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    58
fun prep ths = (Library.filter is_meta_eq ths) @ (map (standard o mk_meta_eq) (Library.filter (not o is_meta_eq) ths))
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    59
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    60
fun inst_tvar ty thm =
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    61
    let
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    62
        val certT = Thm.ctyp_of (Thm.theory_of_thm thm);
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    63
        val ord = prod_ord (prod_ord string_ord int_ord) (list_ord string_ord)
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    64
        val v = TVar (hd (sort ord (term_tvars (prop_of thm))))
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    65
    in
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    66
        standard (Thm.instantiate ([(certT v, certT ty)], []) thm)
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    67
    end
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    68
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    69
fun inst_tvars [] thms = thms
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    70
  | inst_tvars (ty::tys) thms = inst_tvars tys (map (inst_tvar ty) thms)
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    71
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    72
val matrix_compute =
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    73
    let
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    74
        val spvecT = FloatSparseMatrixBuilder.real_spvecT
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    75
        val spmatT = FloatSparseMatrixBuilder.real_spmatT
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    76
        val spvecT_elem = HOLogic.mk_prodT (HOLogic.natT, HOLogic.realT)
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    77
        val spmatT_elem = HOLogic.mk_prodT (HOLogic.natT, spvecT)
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    78
        val case_compute = map thm ["list_case_compute", "list_case_compute_empty", "list_case_compute_cons"]
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    79
        val ths =
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    80
            prep (
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    81
            (inst_tvars [HOLogic.intT, HOLogic.natT] (thms "Let_compute"))
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    82
            @ (inst_tvars [HOLogic.intT, HOLogic.intT] (thms "Let_compute"))
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    83
            @ (map (fn t => inst_tvar t (thm "If_True")) [HOLogic.intT, HOLogic.natT, HOLogic.realT, spvecT, spmatT, HOLogic.boolT])
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    84
            @ (map (fn t => inst_tvar t (thm "If_False")) [HOLogic.intT, HOLogic.natT, HOLogic.realT, spvecT, spmatT, HOLogic.boolT])
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    85
            @ (thms "MatrixLP.float_arith")
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    86
            @ (map (inst_tvar HOLogic.realT) (thms "MatrixLP.sparse_row_matrix_arith_simps"))
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    87
            @ (thms "MatrixLP.boolarith")
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    88
            @ (inst_tvars [HOLogic.natT, HOLogic.realT] [thm "fst_compute", thm "snd_compute"])
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    89
            @ (inst_tvars [HOLogic.natT, FloatSparseMatrixBuilder.real_spvecT] [thm "fst_compute", thm "snd_compute"])
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    90
            @ (inst_tvars [HOLogic.boolT, spmatT_elem] case_compute)
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    91
            @ (inst_tvars [HOLogic.boolT, spvecT_elem] case_compute)
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    92
            @ (inst_tvars [HOLogic.boolT, HOLogic.realT] case_compute)
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    93
            @ (inst_tvars [spvecT] (thms "MatrixLP.sorted_sp_simps"))
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    94
            @ (inst_tvars [HOLogic.realT] (thms "MatrixLP.sorted_sp_simps"))
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    95
            @ [thm "zero_eq_Numeral0_nat", thm "one_eq_Numeral1_nat"]
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    96
            @ (inst_tvars [HOLogic.intT] [thm "zero_eq_Numeral0_nring", thm "one_eq_Numeral1_nring"])
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    97
            @ (inst_tvars [HOLogic.realT] [thm "zero_eq_Numeral0_nring", thm "one_eq_Numeral1_nring"]))
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    98
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    99
        val c = Compute.basic_make (the_context ()) ths
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
   100
    in
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
   101
        Compute.rewrite c
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
   102
    end
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
   103
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
   104
fun matrix_simplify th =
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
   105
    let
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
   106
        val simp_th = matrix_compute (cprop_of th)
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
   107
        val th = strip_shyps (equal_elim simp_th th)
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
   108
        fun removeTrue th = removeTrue (implies_elim th TrueI) handle _ => th
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
   109
    in
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
   110
        removeTrue th
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
   111
    end
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
   112
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
   113
fun prove_bound lptfile prec =
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
   114
    let
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
   115
        val th = lp_dual_estimate_prt lptfile prec
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
   116
    in
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
   117
        matrix_simplify th
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
   118
    end
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
   119
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
   120
val realFromStr = the o Real.fromString;
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
   121
fun float2real (x, y) = realFromStr x * Math.pow (2.0, realFromStr y);
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
   122
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
   123
end