--- a/src/HOL/ex/Lagrange.thy Wed Jan 24 17:10:50 2007 +0100
+++ b/src/HOL/ex/Lagrange.thy Wed Jan 24 20:54:20 2007 +0100
@@ -41,7 +41,7 @@
text {*
- A challenge by John Harrison. Takes about 22s on a 1.6GHz machine.
+ A challenge by John Harrison. Takes about 17s on a 1.6GHz machine.
*}
lemma