| changeset 22173 | 7a78b9531b80 |
| parent 21404 | eb85850d3eb7 |
| child 23477 | f4b83f03cac9 |
| 22172:e7d6cb237b5e | 22173:7a78b9531b80 |
|---|---|
39 sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)" |
39 sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)" |
40 by (simp add: sq_def ring_eq_simps) |
40 by (simp add: sq_def ring_eq_simps) |
41 |
41 |
42 |
42 |
43 text {* |
43 text {* |
44 A challenge by John Harrison. Takes about 22s on a 1.6GHz machine. |
44 A challenge by John Harrison. Takes about 17s on a 1.6GHz machine. |
45 *} |
45 *} |
46 |
46 |
47 lemma |
47 lemma |
48 fixes p1 :: "'a::comm_ring" |
48 fixes p1 :: "'a::comm_ring" |
49 shows |
49 shows |