src/HOL/Hoare/Arith2.thy
changeset 1374 5e407f2a3323
parent 1335 5e1c0540f285
child 1476 608483c2122a
     1.1 --- a/src/HOL/Hoare/Arith2.thy	Wed Nov 29 16:58:30 1995 +0100
     1.2 +++ b/src/HOL/Hoare/Arith2.thy	Wed Nov 29 17:01:41 1995 +0100
     1.3 @@ -9,12 +9,12 @@
     1.4  Arith2 = Arith +
     1.5  
     1.6  consts
     1.7 -  divides :: "[nat, nat] => bool"			(infixl 70)
     1.8 -  cd	  :: "[nat, nat, nat] => bool"
     1.9 -  gcd	  :: "[nat, nat] => nat"
    1.10 +  divides :: [nat, nat] => bool			(infixl 70)
    1.11 +  cd	  :: [nat, nat, nat] => bool
    1.12 +  gcd	  :: [nat, nat] => nat
    1.13  
    1.14 -  pow	  :: "[nat, nat] => nat"			(infixl 75)
    1.15 -  fac	  :: "nat => nat"
    1.16 +  pow	  :: [nat, nat] => nat			(infixl 75)
    1.17 +  fac	  :: nat => nat
    1.18  
    1.19  defs
    1.20    divides_def	"x divides n == 0<n & 0<x & (n mod x) = 0"