equal
deleted
inserted
replaced
163 shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))" |
163 shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))" |
164 by simp |
164 by simp |
165 |
165 |
166 text{*The integers form a @{text comm_ring_1}*} |
166 text{*The integers form a @{text comm_ring_1}*} |
167 |
167 |
168 |
|
169 ML {* val qty = @{typ "int"} *} |
|
170 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
|
171 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "int" *} |
|
172 |
168 |
173 instance int :: comm_ring_1 |
169 instance int :: comm_ring_1 |
174 proof |
170 proof |
175 fix i j k :: int |
171 fix i j k :: int |
176 show "(i + j) + k = i + (j + k)" |
172 show "(i + j) + k = i + (j + k)" |