author | oheimb |
Fri, 20 Feb 1998 16:00:18 +0100 | |
changeset 4637 | bac998af6ea2 |
parent 2281 | e00c13a29eda |
permissions | -rw-r--r-- |
(* Title: HOL/Integ/Lagrange.thy ID: $Id$ Author: Tobias Nipkow Copyright 1996 TU Muenchen This theory only contains a single thm, which is a lemma in Lagrange's proof that every natural number is the sum of 4 squares. It's sole purpose is to demonstrate ordered rewriting for commutative rings. The enterprising reader might consider proving all of Lagrange's thm. *) Lagrange = Ring + constdefs sq :: 'a::times => 'a "sq x == x*x" end