equal
deleted
inserted
replaced
839 unfolding transp_def |
839 unfolding transp_def |
840 by blast |
840 by blast |
841 |
841 |
842 ML {* |
842 ML {* |
843 fun equivp_tac reflps symps transps = |
843 fun equivp_tac reflps symps transps = |
844 let val _ = tracing (PolyML.makestring (reflps, symps, transps)) in |
844 (*let val _ = tracing (PolyML.makestring (reflps, symps, transps)) in *) |
845 simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def}) |
845 simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def}) |
846 THEN' rtac conjI THEN' rtac allI THEN' |
846 THEN' rtac conjI THEN' rtac allI THEN' |
847 resolve_tac reflps THEN' |
847 resolve_tac reflps THEN' |
848 rtac conjI THEN' rtac allI THEN' rtac allI THEN' |
848 rtac conjI THEN' rtac allI THEN' rtac allI THEN' |
849 resolve_tac symps THEN' |
849 resolve_tac symps THEN' |
850 rtac @{thm transpI} THEN' resolve_tac transps |
850 rtac @{thm transpI} THEN' resolve_tac transps |
851 end |
|
852 *} |
851 *} |
853 |
852 |
854 ML {* |
853 ML {* |
855 fun build_equivps alphas reflps alpha_induct term_inj alpha_inj distinct cases eqvt ctxt = |
854 fun build_equivps alphas reflps alpha_induct term_inj alpha_inj distinct cases eqvt ctxt = |
856 let |
855 let |