author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 5078 7b5ea59c0275
child 11375 a6730c90e753
permissions -rw-r--r--
hide many names from Datatype_Universe.

(*  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"