equal
deleted
inserted
replaced
96 text {* \medskip Surjective pairing *} |
96 text {* \medskip Surjective pairing *} |
97 |
97 |
98 lemma "r = (| xpos = xpos r, ypos = ypos r |)" |
98 lemma "r = (| xpos = xpos r, ypos = ypos r |)" |
99 by simp |
99 by simp |
100 |
100 |
101 lemma "r = (| xpos = xpos r, ypos = ypos r, ... = more r |)" |
101 lemma "r = (| xpos = xpos r, ypos = ypos r, ... = point.more r |)" |
102 by simp |
102 by simp |
103 |
103 |
104 |
104 |
105 text {* |
105 text {* |
106 \medskip Representation of records by cases or (degenerate) |
106 \medskip Representation of records by cases or (degenerate) |