| changeset 46783 | 3e89a5cab8d7 |
| parent 44766 | d4d33a4d7548 |
| 46782:d50855d9ea74 | 46783:3e89a5cab8d7 |
|---|---|
203 (\<forall>(x :: int) y z. (x + y = x + z) = (y = z)) \<and> |
203 (\<forall>(x :: int) y z. (x + y = x + z) = (y = z)) \<and> |
204 (\<forall>(w :: int) x y z. (w * y + x * z = w * z + x * y) = (w = x \<or> y = z))" |
204 (\<forall>(w :: int) x y z. (w * y + x * z = w * z + x * y) = (w = x \<or> y = z))" |
205 by (auto simp add: crossproduct_eq) |
205 by (auto simp add: crossproduct_eq) |
206 |
206 |
207 end |
207 end |
208 |