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 equivp_reflp} OF [x]) @{thms alpha_equivps} |
221 val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) @{thms alpha_equivps} |
222 (*val trans2 = map (fn x => @{thm EQUALS_PRS} OF [x]) quot*) |
222 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 |
|
225 *} |
223 *} |
226 |
224 |
227 lemma |
225 lemma |
228 assumes a0: |
226 assumes a0: |
229 "P1 TYP TYP" |
227 "P1 TYP TYP" |