src/HOL/Hoare/Arith2.thy
changeset 5183 89f162de39cf
parent 4359 6f2986464280
child 8791 50b650d19641
equal deleted inserted replaced
5182:69917bbbce45 5183:89f162de39cf
    14 
    14 
    15   gcd     :: [nat, nat] => nat
    15   gcd     :: [nat, nat] => nat
    16   "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
    16   "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
    17 
    17 
    18 consts fac     :: nat => nat
    18 consts fac     :: nat => nat
    19 primrec fac nat
    19 
    20 "fac 0 = Suc 0"
    20 primrec
    21 "fac(Suc n) = (Suc n)*fac(n)"
    21   "fac 0 = Suc 0"
       
    22   "fac(Suc n) = (Suc n)*fac(n)"
    22 
    23 
    23 end
    24 end