equal
deleted
inserted
replaced
712 in if (pbeta_redex Q) (length vlist) |
712 in if (pbeta_redex Q) (length vlist) |
713 then pq_eliminate (thm,thy,vlist,imp_body,Q) |
713 then pq_eliminate (thm,thy,vlist,imp_body,Q) |
714 else |
714 else |
715 let val tych = cterm_of thy |
715 let val tych = cterm_of thy |
716 val ants1 = map tych ants |
716 val ants1 = map tych ants |
717 val ss' = MetaSimplifier.add_prems (map ASSUME ants1) ss |
717 val ss' = Simplifier.add_prems (map ASSUME ants1) ss |
718 val Q_eeq_Q1 = MetaSimplifier.rewrite_cterm |
718 val Q_eeq_Q1 = MetaSimplifier.rewrite_cterm |
719 (false,true,false) (prover used') ss' (tych Q) |
719 (false,true,false) (prover used') ss' (tych Q) |
720 handle Utils.ERR _ => Thm.reflexive (tych Q) |
720 handle Utils.ERR _ => Thm.reflexive (tych Q) |
721 val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1 |
721 val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1 |
722 val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq |
722 val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq |