diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/Hoare/Arith2.thy --- a/src/HOL/Hoare/Arith2.thy Mon Feb 05 21:27:16 1996 +0100 +++ b/src/HOL/Hoare/Arith2.thy Mon Feb 05 21:29:06 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/Hoare/Arith2.thy +(* Title: HOL/Hoare/Arith2.thy ID: \$Id\$ - Author: Norbert Galm + Author: Norbert Galm Copyright 1995 TUM More arithmetic. @@ -9,19 +9,19 @@ Arith2 = Arith + consts - divides :: [nat, nat] => bool (infixl 70) - cd :: [nat, nat, nat] => bool - gcd :: [nat, nat] => nat + divides :: [nat, nat] => bool (infixl 70) + cd :: [nat, nat, nat] => bool + gcd :: [nat, nat] => nat - pow :: [nat, nat] => nat (infixl 75) - fac :: nat => nat + pow :: [nat, nat] => nat (infixl 75) + fac :: nat => nat defs - divides_def "x divides n == 0 y<=x)" + divides_def "x divides n == 0 y<=x)" - pow_def "m pow n == nat_rec n (Suc 0) (%u v.m*v)" - fac_def "fac m == nat_rec m (Suc 0) (%u v.(Suc u)*v)" + pow_def "m pow n == nat_rec n (Suc 0) (%u v.m*v)" + fac_def "fac m == nat_rec m (Suc 0) (%u v.(Suc u)*v)" end