equal
deleted
inserted
replaced
217 thm kind_ty_trm.induct |
217 thm kind_ty_trm.induct |
218 |
218 |
219 ML {* |
219 ML {* |
220 val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} |
220 val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} |
221 val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs} |
221 val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs} |
222 val trans2 = map (fn x => @{thm EQUALS_PRS} OF [x]) quot |
222 (*val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) @{thms alpha_EQUIVs}*) |
223 val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot |
223 val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot |
224 val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same |
224 val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same |
225 *} |
225 *} |
226 |
226 |
227 lemma |
227 lemma |