src/HOL/Hoare/Arith2.thy
changeset 1476 608483c2122a
parent 1374 5e407f2a3323
child 1558 9c6ebfab4e05
     1.1 --- a/src/HOL/Hoare/Arith2.thy	Mon Feb 05 21:27:16 1996 +0100
     1.2 +++ b/src/HOL/Hoare/Arith2.thy	Mon Feb 05 21:29:06 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	HOL/Hoare/Arith2.thy
     1.5 +(*  Title:      HOL/Hoare/Arith2.thy
     1.6      ID:         $Id$
     1.7 -    Author: 	Norbert Galm
     1.8 +    Author:     Norbert Galm
     1.9      Copyright   1995 TUM
    1.10  
    1.11  More arithmetic.
    1.12 @@ -9,19 +9,19 @@
    1.13  Arith2 = Arith +
    1.14  
    1.15  consts
    1.16 -  divides :: [nat, nat] => bool			(infixl 70)
    1.17 -  cd	  :: [nat, nat, nat] => bool
    1.18 -  gcd	  :: [nat, nat] => nat
    1.19 +  divides :: [nat, nat] => bool                 (infixl 70)
    1.20 +  cd      :: [nat, nat, nat] => bool
    1.21 +  gcd     :: [nat, nat] => nat
    1.22  
    1.23 -  pow	  :: [nat, nat] => nat			(infixl 75)
    1.24 -  fac	  :: nat => nat
    1.25 +  pow     :: [nat, nat] => nat                  (infixl 75)
    1.26 +  fac     :: nat => nat
    1.27  
    1.28  defs
    1.29 -  divides_def	"x divides n == 0<n & 0<x & (n mod x) = 0"
    1.30 -  cd_def	"cd x m n  == x divides m & x divides n"
    1.31 -  gcd_def	"gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
    1.32 +  divides_def   "x divides n == 0<n & 0<x & (n mod x) = 0"
    1.33 +  cd_def        "cd x m n  == x divides m & x divides n"
    1.34 +  gcd_def       "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
    1.35  
    1.36 -  pow_def	"m pow n     == nat_rec n (Suc 0) (%u v.m*v)"
    1.37 -  fac_def	"fac m       == nat_rec m (Suc 0) (%u v.(Suc u)*v)"
    1.38 +  pow_def       "m pow n     == nat_rec n (Suc 0) (%u v.m*v)"
    1.39 +  fac_def       "fac m       == nat_rec m (Suc 0) (%u v.(Suc u)*v)"
    1.40  
    1.41  end