changeset 25475 | d5a382ccb5cc |
parent 23477 | f4b83f03cac9 |
child 26480 | 544cef16045b |
--- a/src/HOL/ex/Lagrange.thy Tue Nov 27 16:48:35 2007 +0100 +++ b/src/HOL/ex/Lagrange.thy Tue Nov 27 16:48:37 2007 +0100 @@ -38,7 +38,7 @@ by (simp add: sq_def ring_simps) -text {* A challenge by John Harrison. Takes about 17s on a 1.6GHz machine. *} +text {* A challenge by John Harrison. Takes about 12s on a 1.6GHz machine. *} lemma fixes p1 :: "'a::comm_ring" shows "(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) *