equal
deleted
inserted
replaced
79 end |
79 end |
80 |
80 |
81 fun matrix_simplify th = |
81 fun matrix_simplify th = |
82 let |
82 let |
83 val simp_th = matrix_compute (cprop_of th) |
83 val simp_th = matrix_compute (cprop_of th) |
84 val th = Thm.strip_shyps (equal_elim simp_th th) |
84 val th = Thm.strip_shyps (Thm.equal_elim simp_th th) |
85 fun removeTrue th = removeTrue (implies_elim th TrueI) handle _ => th (* FIXME avoid handle _ *) |
85 fun removeTrue th = removeTrue (Thm.implies_elim th TrueI) handle _ => th (* FIXME avoid handle _ *) |
86 in |
86 in |
87 removeTrue th |
87 removeTrue th |
88 end |
88 end |
89 |
89 |
90 fun prove_bound lptfile prec = |
90 fun prove_bound lptfile prec = |