author  wenzelm 
Thu Jan 23 14:19:16 1997 +0100 (19970123)  
changeset 2545  d10abc8c11fb 
parent 2281  e00c13a29eda 
permissions  rwrr 
nipkow@2281  1 
(* Title: HOL/Integ/Lagrange.thy 
nipkow@2281  2 
ID: $Id$ 
nipkow@2281  3 
Author: Tobias Nipkow 
nipkow@2281  4 
Copyright 1996 TU Muenchen 
nipkow@2281  5 

nipkow@2281  6 

nipkow@2281  7 
This theory only contains a single thm, which is a lemma in Lagrange's proof 
nipkow@2281  8 
that every natural number is the sum of 4 squares. It's sole purpose is to 
nipkow@2281  9 
demonstrate ordered rewriting for commutative rings. 
nipkow@2281  10 

nipkow@2281  11 
The enterprising reader might consider proving all of Lagrange's thm. 
nipkow@2281  12 
*) 
nipkow@2281  13 
Lagrange = Ring + 
nipkow@2281  14 

nipkow@2281  15 
constdefs sq :: 'a::times => 'a 
nipkow@2281  16 
"sq x == x*x" 
nipkow@2281  17 

nipkow@2281  18 
end 