| author | berghofe |
| Mon, 11 Jun 2001 19:21:13 +0200 | |
| changeset 11371 | 1d5d181b7e28 |
| parent 5078 | 7b5ea59c0275 |
| child 11375 | a6730c90e753 |
| permissions | -rw-r--r-- |
| 5078 | 1 |
(* Title: HOL/Integ/Lagrange.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1996 TU Muenchen |
|
5 |
||
6 |
||
7 |
This theory only contains a single thm, which is a lemma in Lagrange's proof |
|
8 |
that every natural number is the sum of 4 squares. It's sole purpose is to |
|
9 |
demonstrate ordered rewriting for commutative rings. |
|
10 |
||
11 |
The enterprising reader might consider proving all of Lagrange's thm. |
|
12 |
*) |
|
13 |
Lagrange = Ring + |
|
14 |
||
15 |
constdefs sq :: 'a::times => 'a |
|
16 |
"sq x == x*x" |
|
17 |
||
18 |
end |