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