equal
deleted
inserted
replaced
156 next |
156 next |
157 assume "x = y" |
157 assume "x = y" |
158 thus "x == y" by (rule eq_reflection) |
158 thus "x == y" by (rule eq_reflection) |
159 qed |
159 qed |
160 |
160 |
|
161 declare atomize_all [symmetric, rulify] atomize_imp [symmetric, rulify] |
|
162 |
161 end |
163 end |