summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/ex/Lagrange.thy

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" end