isabelle: src/HOL/Integ/Lagrange.thy@749600cb5573 (annotated)

2281 e00c13a29eda Ring Theory. nipkow parents: diff changeset	1	(* Title: HOL/Integ/Lagrange.thy
e00c13a29eda Ring Theory. nipkow parents: diff changeset	2	ID: $Id$
e00c13a29eda Ring Theory. nipkow parents: diff changeset	3	Author: Tobias Nipkow
e00c13a29eda Ring Theory. nipkow parents: diff changeset	4	Copyright 1996 TU Muenchen
e00c13a29eda Ring Theory. nipkow parents: diff changeset	5
e00c13a29eda Ring Theory. nipkow parents: diff changeset	6
e00c13a29eda Ring Theory. nipkow parents: diff changeset	7	This theory only contains a single thm, which is a lemma in Lagrange's proof
e00c13a29eda Ring Theory. nipkow parents: diff changeset	8	that every natural number is the sum of 4 squares. It's sole purpose is to
e00c13a29eda Ring Theory. nipkow parents: diff changeset	9	demonstrate ordered rewriting for commutative rings.
e00c13a29eda Ring Theory. nipkow parents: diff changeset	10
e00c13a29eda Ring Theory. nipkow parents: diff changeset	11	The enterprising reader might consider proving all of Lagrange's thm.
e00c13a29eda Ring Theory. nipkow parents: diff changeset	12	*)
e00c13a29eda Ring Theory. nipkow parents: diff changeset	13	Lagrange = Ring +
e00c13a29eda Ring Theory. nipkow parents: diff changeset	14
e00c13a29eda Ring Theory. nipkow parents: diff changeset	15	constdefs sq :: 'a::times => 'a
e00c13a29eda Ring Theory. nipkow parents: diff changeset	16	"sq x == x*x"
e00c13a29eda Ring Theory. nipkow parents: diff changeset	17
e00c13a29eda Ring Theory. nipkow parents: diff changeset	18	end

author	wenzelm
	Sun, 28 Dec 1997 14:58:56 +0100
changeset 4489	749600cb5573
parent 2281	e00c13a29eda
permissions	-rw-r--r--