src/HOL/Hoare/Arith2.thy
changeset 17278 f27456a2a975
parent 8791 50b650d19641
child 19802 c2860c37e574
     1.1 --- a/src/HOL/Hoare/Arith2.thy	Tue Sep 06 16:59:52 2005 +0200
     1.2 +++ b/src/HOL/Hoare/Arith2.thy	Tue Sep 06 16:59:53 2005 +0200
     1.3 @@ -6,19 +6,23 @@
     1.4  More arithmetic.  Much of this duplicates ex/Primes.
     1.5  *)
     1.6  
     1.7 -Arith2 = Main +
     1.8 +theory Arith2
     1.9 +imports Main
    1.10 +begin
    1.11  
    1.12  constdefs
    1.13 -  cd      :: [nat, nat, nat] => bool
    1.14 +  "cd"    :: "[nat, nat, nat] => bool"
    1.15    "cd x m n  == x dvd m & x dvd n"
    1.16  
    1.17 -  gcd     :: [nat, nat] => nat
    1.18 +  gcd     :: "[nat, nat] => nat"
    1.19    "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
    1.20  
    1.21 -consts fac     :: nat => nat
    1.22 +consts fac     :: "nat => nat"
    1.23  
    1.24  primrec
    1.25    "fac 0 = Suc 0"
    1.26    "fac(Suc n) = (Suc n)*fac(n)"
    1.27  
    1.28 +ML {* use_legacy_bindings (the_context ()) *}
    1.29 +
    1.30  end