| changeset 3018 | e65b60b28341 |
| parent 2281 | e00c13a29eda |
| child 5069 | 3ea049f7979d |
--- a/src/HOL/Integ/IntRing.ML Wed Apr 23 11:00:48 1997 +0200 +++ b/src/HOL/Integ/IntRing.ML Wed Apr 23 11:02:19 1997 +0200 @@ -14,5 +14,5 @@ \ sq(i1*j2 + i2*j1 + i3*j4 - i4*j3) + \ \ sq(i1*j3 - i2*j4 + i3*j1 + i4*j2) + \ \ sq(i1*j4 + i2*j3 - i3*j2 + i4*j1)"; -br Lagrange_lemma 1; +by (rtac Lagrange_lemma 1); qed "Lagrange_lemma_int";