equal
deleted
inserted
replaced
129 fun DISCH_ALL thm = fold_rev DISCH (#hyps (Thm.crep_thm thm)) thm; |
129 fun DISCH_ALL thm = fold_rev DISCH (#hyps (Thm.crep_thm thm)) thm; |
130 |
130 |
131 |
131 |
132 fun FILTER_DISCH_ALL P thm = |
132 fun FILTER_DISCH_ALL P thm = |
133 let fun check tm = P (#t (Thm.rep_cterm tm)) |
133 let fun check tm = P (#t (Thm.rep_cterm tm)) |
134 in List.foldr (fn (tm,th) => if check tm then DISCH tm th else th) |
134 in fold_rev (fn tm => fn th => if check tm then DISCH tm th else th) (chyps thm) thm |
135 thm (chyps thm) |
|
136 end; |
135 end; |
137 |
136 |
138 (* freezeT expensive! *) |
137 (* freezeT expensive! *) |
139 fun UNDISCH thm = |
138 fun UNDISCH thm = |
140 let val tm = D.mk_prop (#1 (D.dest_imp (cconcl (Thm.freezeT thm)))) |
139 let val tm = D.mk_prop (#1 (D.dest_imp (cconcl (Thm.freezeT thm)))) |