equal
deleted
inserted
replaced
493 fun equal_implies_1_rule PQ = |
493 fun equal_implies_1_rule PQ = |
494 let |
494 let |
495 val P = Thm.lhs_of PQ |
495 val P = Thm.lhs_of PQ |
496 in Thm.implies_intr P (Thm.equal_elim PQ (Thm.assume P)) |
496 in Thm.implies_intr P (Thm.equal_elim PQ (Thm.assume P)) |
497 end |
497 end |
498 (* FIXME!!! Copied from groebner.ml *) |
498 (*FIXME!!! Copied from groebner.ml*) |
499 val strip_exists = |
499 val strip_exists = |
500 let |
500 let |
501 fun h (acc, t) = |
501 fun h (acc, t) = |
502 case Thm.term_of t of |
502 case Thm.term_of t of |
503 Const(@{const_name Ex},_)$Abs(_,_,_) => |
503 Const(@{const_name Ex},_)$Abs(_,_,_) => |