equal
deleted
inserted
replaced
4 |
4 |
5 signature MATRIX_LP = |
5 signature MATRIX_LP = |
6 sig |
6 sig |
7 val matrix_compute : cterm -> thm |
7 val matrix_compute : cterm -> thm |
8 val matrix_simplify : thm -> thm |
8 val matrix_simplify : thm -> thm |
9 val prove_bound : string -> int -> thm |
|
10 val float2real : string * string -> Real.real |
|
11 end |
9 end |
12 |
10 |
13 structure MatrixLP : MATRIX_LP = |
11 structure MatrixLP : MATRIX_LP = |
14 struct |
12 struct |
15 |
13 |
51 removeTrue th |
49 removeTrue th |
52 end |
50 end |
53 |
51 |
54 val prove_bound = matrix_simplify oo lp_dual_estimate_prt; |
52 val prove_bound = matrix_simplify oo lp_dual_estimate_prt; |
55 |
53 |
56 val realFromStr = the o Real.fromString; |
|
57 fun float2real (x, y) = realFromStr x * Math.pow (2.0, realFromStr y); |
|
58 |
|
59 end |
54 end |