Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
challenge by John Harrison: down to 12s (was 17s, was 75s);
authorwenzelm
Tue, 27 Nov 2007 16:48:37 +0100
changeset 25475 d5a382ccb5cc
parent 25474 c41b433b0f65
child 25476 03da46cfab9e
challenge by John Harrison: down to 12s (was 17s, was 75s);
src/HOL/ex/Lagrange.thy file | annotate | diff | comparison | revisions 
--- 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) *
isabelle