equal
deleted
inserted
replaced
71 shows "equivp akind" |
71 shows "equivp akind" |
72 and "equivp aty" |
72 and "equivp aty" |
73 and "equivp atrm" |
73 and "equivp atrm" |
74 sorry |
74 sorry |
75 |
75 |
76 quotient KIND = kind / akind |
76 quotient_type KIND = kind / akind |
77 by (rule alpha_equivps) |
77 by (rule alpha_equivps) |
78 |
78 |
79 quotient TY = ty / aty |
79 quotient_type |
80 and TRM = trm / atrm |
80 TY = ty / aty and |
|
81 TRM = trm / atrm |
81 by (auto intro: alpha_equivps) |
82 by (auto intro: alpha_equivps) |
82 |
83 |
83 quotient_def |
84 quotient_def |
84 "TYP :: KIND" |
85 "TYP :: KIND" |
85 as |
86 as |