| changeset 39795 | 9e59b4c11039 |
| parent 39128 | 93a7365fb4ee |
| child 41413 | 64cd30d6b0b8 |
| 39794:51451d73c3d4 | 39795:9e59b4c11039 |
|---|---|
93 |
93 |
94 |
94 |
95 text{* |
95 text{* |
96 set extensionality |
96 set extensionality |
97 |
97 |
98 @{thm[display] set_ext[no_vars]} |
98 @{thm[display] set_eqI[no_vars]} |
99 \rulename{set_ext} |
99 \rulename{set_eqI} |
100 |
100 |
101 @{thm[display] equalityI[no_vars]} |
101 @{thm[display] equalityI[no_vars]} |
102 \rulename{equalityI} |
102 \rulename{equalityI} |
103 |
103 |
104 @{thm[display] equalityE[no_vars]} |
104 @{thm[display] equalityE[no_vars]} |