author | berghofe |
Fri, 24 Jul 1998 13:03:20 +0200 | |
changeset 5183 | 89f162de39cf |
parent 4359 | 6f2986464280 |
child 8791 | 50b650d19641 |
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 = Power + 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