summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Integ/Lagrange.thy

author | wenzelm |

Thu Jan 23 14:19:16 1997 +0100 (1997-01-23) | |

changeset 2545 | d10abc8c11fb |

parent 2281 | e00c13a29eda |

permissions | -rw-r--r-- |

added AxClasses test;

1 (* Title: HOL/Integ/Lagrange.thy

2 ID: $Id$

3 Author: Tobias Nipkow

4 Copyright 1996 TU Muenchen

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.

11 The enterprising reader might consider proving all of Lagrange's thm.

12 *)

13 Lagrange = Ring +

15 constdefs sq :: 'a::times => 'a

16 "sq x == x*x"

18 end