| changeset 40607 | 30d512bf47a7 |
| parent 38795 | 848be46708dc |
| child 41589 | bbd861837ebc |
| 40606:af1a0b0c6202 | 40607:30d512bf47a7 |
|---|---|
129 "," > Pair |
129 "," > Pair |
130 FST > fst |
130 FST > fst |
131 SND > snd |
131 SND > snd |
132 CURRY > curry |
132 CURRY > curry |
133 UNCURRY > split |
133 UNCURRY > split |
134 "##" > prod_fun |
134 "##" > map_pair |
135 pair_case > split; |
135 pair_case > split; |
136 |
136 |
137 ignore_thms |
137 ignore_thms |
138 prod_TY_DEF |
138 prod_TY_DEF |
139 MK_PAIR_DEF |
139 MK_PAIR_DEF |