src/HOL/Hoare/Arith2.thy

theorem(_i): empty target;
forget_proof: removed tmp hack;

(*  Title:      HOL/Hoare/Arith2.thy
    ID:         $Id$
    Author:     Norbert Galm
    Copyright   1995 TUM

More arithmetic.  Much of this duplicates ex/Primes.
*)

theory Arith2
imports Main
begin

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)"

ML {* use_legacy_bindings (the_context ()) *}

end