src/HOL/Hoare/Arith2.thy
 changeset 1476 608483c2122a parent 1374 5e407f2a3323 child 1558 9c6ebfab4e05
```--- 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

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

-  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```