| changeset 12815 | 1f073030b97a |
| parent 10864 | f0b0a125ae4b |
| child 16417 | 9bc16273c2d4 |
| 12814:2f5edb146f7e | 12815:1f073030b97a |
|---|---|
88 by blast |
88 by blast |
89 |
89 |
90 text{*A type constraint lets it work*} |
90 text{*A type constraint lets it work*} |
91 |
91 |
92 text{*An issue here: how do we discuss the distinction between ASCII and |
92 text{*An issue here: how do we discuss the distinction between ASCII and |
93 X-symbol notation? Here the latter disambiguates.*} |
93 symbol notation? Here the latter disambiguates.*} |
94 |
94 |
95 |
95 |
96 text{* |
96 text{* |
97 set extensionality |
97 set extensionality |
98 |
98 |