src/HOL/Old_Number_Theory/IntFact.thy
changeset 38159 e9b4835a54ee
parent 35440 bdf8ad377877
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Old_Number_Theory/IntFact.thy	Thu Aug 05 23:43:43 2010 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/IntFact.thy	Fri Aug 06 12:37:00 2010 +0200
     1.3 @@ -1,10 +1,13 @@
     1.4 -(*  Author:     Thomas M. Rasmussen
     1.5 +(*  Title:      HOL/Old_Number_Theory/IntFact.thy
     1.6 +    Author:     Thomas M. Rasmussen
     1.7      Copyright   2000  University of Cambridge
     1.8  *)
     1.9  
    1.10  header {* Factorial on integers *}
    1.11  
    1.12 -theory IntFact imports IntPrimes begin
    1.13 +theory IntFact
    1.14 +imports IntPrimes
    1.15 +begin
    1.16  
    1.17  text {*
    1.18    Factorial on integers and recursively defined set including all
    1.19 @@ -14,15 +17,11 @@
    1.20    \bigskip
    1.21  *}
    1.22  
    1.23 -fun
    1.24 -  zfact :: "int => int"
    1.25 -where
    1.26 -  "zfact n = (if n \<le> 0 then 1 else n * zfact (n - 1))"
    1.27 +fun zfact :: "int => int"
    1.28 +  where "zfact n = (if n \<le> 0 then 1 else n * zfact (n - 1))"
    1.29  
    1.30 -fun
    1.31 -  d22set :: "int => int set"
    1.32 -where
    1.33 -  "d22set a = (if 1 < a then insert a (d22set (a - 1)) else {})"
    1.34 +fun d22set :: "int => int set"
    1.35 +  where "d22set a = (if 1 < a then insert a (d22set (a - 1)) else {})"
    1.36  
    1.37  
    1.38  text {*