# HG changeset patch
# User haftmann
# Date 1279548583 -7200
# Node ID c43805c80eb6c8ea194d0bba905d89032ae34ea0
# Parent  314a88278715680e2e3d8686d2b778a3d194c4c0
dropped essentially ineffective tuning

diff -r 314a88278715 -r c43805c80eb6 src/HOL/ex/Lagrange.thy
--- a/src/HOL/ex/Lagrange.thy	Mon Jul 19 16:09:43 2010 +0200
+++ b/src/HOL/ex/Lagrange.thy	Mon Jul 19 16:09:43 2010 +0200
@@ -22,12 +22,6 @@
 However, this is an abstract theorem about commutative rings.  It has,
 a priori, nothing to do with nat. *}
 
-(* These two simprocs are even less efficient than ordered rewriting
-   and kill the second example: *)
-ML {*
-  Delsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
-*}
-
 lemma Lagrange_lemma: fixes x1 :: "'a::comm_ring" shows
   "(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
    sq (x1*y1 - x2*y2 - x3*y3 - x4*y4)  +