src/HOL/Hoare/Arith2.thy
 changeset 1558 9c6ebfab4e05 parent 1476 608483c2122a child 1824 44254696843a
```--- a/src/HOL/Hoare/Arith2.thy	Wed Mar 06 14:19:39 1996 +0100
+++ b/src/HOL/Hoare/Arith2.thy	Fri Mar 08 13:11:09 1996 +0100
@@ -8,20 +8,20 @@

Arith2 = Arith +

-consts
-  divides :: [nat, nat] => bool                 (infixl 70)
+constdefs
+  divides :: [nat, nat] => bool                             (infixl 70)
+  "x divides n == 0<n & 0<x & (n mod x) = 0"
+
cd      :: [nat, nat, nat] => bool
-  gcd     :: [nat, nat] => nat
-
-  pow     :: [nat, nat] => nat                  (infixl 75)
-  fac     :: nat => nat
+  "cd x m n  == x divides m & x divides n"

-defs
-  divides_def   "x divides n == 0<n & 0<x & (n mod x) = 0"
-  cd_def        "cd x m n  == x divides m & x divides n"
-  gcd_def       "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
+  gcd     :: [nat, nat] => nat
+  "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> 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     :: [nat, nat] => nat                              (infixl 75)
+  "m pow n     == nat_rec n (Suc 0) (%u v.m*v)"
+
+  fac     :: nat => nat
+  "fac m       == nat_rec m (Suc 0) (%u v.(Suc u)*v)"

end```