equal
deleted
inserted
replaced
707 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps rsp_thms)) |
707 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps rsp_thms)) |
708 THEN_ALL_NEW (fn _ => no_tac) |
708 THEN_ALL_NEW (fn _ => no_tac) |
709 ), |
709 ), |
710 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
710 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
711 rtac refl, |
711 rtac refl, |
|
712 rtac @{thm arg_cong2[of _ _ _ _ "op ="]}, |
712 (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
713 (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
713 rtac reflex_thm, |
714 rtac reflex_thm, |
714 atac, |
715 atac, |
715 ( |
716 ( |
716 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
717 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
785 in |
786 in |
786 map Thm.varifyT defs_sym |
787 map Thm.varifyT defs_sym |
787 end |
788 end |
788 *} |
789 *} |
789 |
790 |
|
791 text {* the proper way to do it *} |
|
792 ML {* |
|
793 fun findabs rty tm = |
|
794 case tm of |
|
795 Abs(_, T, b) => |
|
796 let |
|
797 val b' = subst_bound ((Free ("x", T)), b); |
|
798 val tys = findabs rty b' |
|
799 val ty = fastype_of tm |
|
800 in if needs_lift rty ty then (ty :: tys) else tys |
|
801 end |
|
802 | f $ a => (findabs rty f) @ (findabs rty a) |
|
803 | _ => [] |
|
804 *} |
790 |
805 |
791 end |
806 end |