isabelle: src/HOL/Hoare/Arith2.thy@d55e2fee2084 (annotated)

1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1374 diff changeset	1	(* Title: HOL/Hoare/Arith2.thy
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	2	ID: $Id$
1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1374 diff changeset	3	Author: Norbert Galm
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	4	Copyright 1995 TUM
5e1c0540f285 New directory. nipkow parents: diff changeset	5
3372 6e472c8f0011 Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs paulson parents: 1824 diff changeset	6	More arithmetic. Much of this duplicates ex/Primes.
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	7	*)
5e1c0540f285 New directory. nipkow parents: diff changeset	8
4359 6f2986464280 Simplified proofs. nipkow parents: 3842 diff changeset	9	Arith2 = Power +
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	10
1558 9c6ebfab4e05 added constdefs section clasohm parents: 1476 diff changeset	11	constdefs
1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1374 diff changeset	12	cd :: [nat, nat, nat] => bool
3372 6e472c8f0011 Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs paulson parents: 1824 diff changeset	13	"cd x m n == x dvd m & x dvd n"
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	14
1558 9c6ebfab4e05 added constdefs section clasohm parents: 1476 diff changeset	15	gcd :: [nat, nat] => nat
9c6ebfab4e05 added constdefs section clasohm parents: 1476 diff changeset	16	"gcd m n == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	17
4359 6f2986464280 Simplified proofs. nipkow parents: 3842 diff changeset	18	consts fac :: nat => nat
6f2986464280 Simplified proofs. nipkow parents: 3842 diff changeset	19	primrec fac nat
6f2986464280 Simplified proofs. nipkow parents: 3842 diff changeset	20	"fac 0 = Suc 0"
6f2986464280 Simplified proofs. nipkow parents: 3842 diff changeset	21	"fac(Suc n) = (Suc n)*fac(n)"
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	22
5e1c0540f285 New directory. nipkow parents: diff changeset	23	end

author	paulson
	Mon, 20 Apr 1998 10:38:30 +0200
changeset 4810	d55e2fee2084
parent 4359	6f2986464280
child 5183	89f162de39cf
permissions	-rw-r--r--