author | nipkow |
Tue, 07 Jan 2003 14:32:04 +0100 | |
changeset 13773 | 58dc4ab362d0 |
parent 8791 | 50b650d19641 |
child 17278 | f27456a2a975 |
permissions | -rw-r--r-- |
(* Title: HOL/Hoare/Arith2.thy ID: $Id$ Author: Norbert Galm Copyright 1995 TUM More arithmetic. Much of this duplicates ex/Primes. *) Arith2 = Main + constdefs cd :: [nat, nat, nat] => bool "cd x m n == x dvd m & x dvd n" gcd :: [nat, nat] => nat "gcd m n == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)" consts fac :: nat => nat primrec "fac 0 = Suc 0" "fac(Suc n) = (Suc n)*fac(n)" end