# HG changeset patch
# User nipkow
# Date 1090332465 -7200
# Node ID 0a0371b55a0f47fd8810a7cb5e90921fb3fe3646
# Parent  58d216b32199b4f515932d033fe5db3301e82a95
ring_1 -> ring

diff -r 58d216b32199 -r 0a0371b55a0f src/HOL/ex/Lagrange.thy
--- a/src/HOL/ex/Lagrange.thy	Tue Jul 20 14:24:23 2004 +0200
+++ b/src/HOL/ex/Lagrange.thy	Tue Jul 20 16:07:45 2004 +0200
@@ -23,7 +23,7 @@
 
 (*once a slow step, but now (2001) just three seconds!*)
 lemma Lagrange_lemma:
- "!!x1::'a::comm_ring_1.
+ "!!x1::'a::comm_ring.
   (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)  +
   sq(x1*y2 + x2*y1 + x3*y4 - x4*y3)  +
@@ -34,7 +34,7 @@
 
 (* A challenge by John Harrison. Takes about 4 mins on a 3GHz machine.
 
-lemma "!!p1::'a::comm_ring_1.
+lemma "!!p1::'a::comm_ring.
  (sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * 
  (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2) 
   = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) +