author | paulson |
Wed, 13 Jun 2001 16:30:12 +0200 | |
changeset 11375 | a6730c90e753 |
parent 5078 | 7b5ea59c0275 |
child 14603 | 985eb6708207 |
permissions | -rw-r--r-- |
(* Title: HOL/ex/Lagrange.thy ID: $Id$ Author: Tobias Nipkow Copyright 1996 TU Muenchen This theory only contains a single theorem, which is a lemma in Lagrange's proof that every natural number is the sum of 4 squares. Its sole purpose is to demonstrate ordered rewriting for commutative rings. The enterprising reader might consider proving all of Lagrange's theorem. *) Lagrange = Ring + constdefs sq :: 'a::times => 'a "sq x == x*x" end