isabelle: src/HOL/Hoare/Arith2.thy@8408a06590a6 (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
8791 50b650d19641 changed 2 to #2 paulson parents: 5183 diff changeset	9	Arith2 = Main +
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
5183 89f162de39cf Adapted to new datatype package. berghofe parents: 4359 diff changeset	19
89f162de39cf Adapted to new datatype package. berghofe parents: 4359 diff changeset	20	primrec
89f162de39cf Adapted to new datatype package. berghofe parents: 4359 diff changeset	21	"fac 0 = Suc 0"
89f162de39cf Adapted to new datatype package. berghofe parents: 4359 diff changeset	22	"fac(Suc n) = (Suc n)*fac(n)"
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	23
5e1c0540f285 New directory. nipkow parents: diff changeset	24	end

author	paulson
	Tue, 29 Mar 2005 12:30:48 +0200
changeset 15635	8408a06590a6
parent 8791	50b650d19641
child 17278	f27456a2a975
permissions	-rw-r--r--