isabelle: src/HOL/Hoare/Arith2.thy@1574533861b1 (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
17278 f27456a2a975 converted to Isar theory format; wenzelm parents: 8791 diff changeset	9	theory Arith2
f27456a2a975 converted to Isar theory format; wenzelm parents: 8791 diff changeset	10	imports Main
f27456a2a975 converted to Isar theory format; wenzelm parents: 8791 diff changeset	11	begin
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	12
1558 9c6ebfab4e05 added constdefs section clasohm parents: 1476 diff changeset	13	constdefs
17278 f27456a2a975 converted to Isar theory format; wenzelm parents: 8791 diff changeset	14	"cd" :: "[nat, nat, nat] => bool"
3372 6e472c8f0011 Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs paulson parents: 1824 diff changeset	15	"cd x m n == x dvd m & x dvd n"
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	16
17278 f27456a2a975 converted to Isar theory format; wenzelm parents: 8791 diff changeset	17	gcd :: "[nat, nat] => nat"
1558 9c6ebfab4e05 added constdefs section clasohm parents: 1476 diff changeset	18	"gcd m n == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	19
17278 f27456a2a975 converted to Isar theory format; wenzelm parents: 8791 diff changeset	20	consts fac :: "nat => nat"
5183 89f162de39cf Adapted to new datatype package. berghofe parents: 4359 diff changeset	21
89f162de39cf Adapted to new datatype package. berghofe parents: 4359 diff changeset	22	primrec
89f162de39cf Adapted to new datatype package. berghofe parents: 4359 diff changeset	23	"fac 0 = Suc 0"
89f162de39cf Adapted to new datatype package. berghofe parents: 4359 diff changeset	24	"fac(Suc n) = (Suc n)*fac(n)"
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	25
17278 f27456a2a975 converted to Isar theory format; wenzelm parents: 8791 diff changeset	26	ML {* use_legacy_bindings (the_context ()) *}
f27456a2a975 converted to Isar theory format; wenzelm parents: 8791 diff changeset	27
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	28	end

author	mengj
	Wed, 19 Oct 2005 06:33:24 +0200
changeset 17905	1574533861b1
parent 17278	f27456a2a975
child 19802	c2860c37e574
permissions	-rw-r--r--