equal
deleted
inserted
replaced
71 fun removeTrue th = removeTrue (implies_elim th TrueI) handle _ => th |
71 fun removeTrue th = removeTrue (implies_elim th TrueI) handle _ => th |
72 in |
72 in |
73 removeTrue th |
73 removeTrue th |
74 end |
74 end |
75 |
75 |
|
76 end |
|
77 |
76 fun float2real (x,y) = (Real.fromInt x) * (Math.pow (2.0, Real.fromInt y)) |
78 fun float2real (x,y) = (Real.fromInt x) * (Math.pow (2.0, Real.fromInt y)) |
77 |
|
78 end |
|
79 |
79 |
80 val result = ref ([]:thm list) |
80 val result = ref ([]:thm list) |
81 |
81 |
82 fun run c = timeit (fn () => (result := [MatrixLP.simplify c]; ())) |
82 fun run c = timeit (fn () => (result := [MatrixLP.simplify c]; ())) |
83 |
83 |