src/HOL/Old_Number_Theory/IntFact.thy
 changeset 61382 efac889fccbc parent 58889 5b7a9633cfa8 child 63167 0909deb8059b
```     1.1 --- a/src/HOL/Old_Number_Theory/IntFact.thy	Sat Oct 10 16:21:34 2015 +0200
1.2 +++ b/src/HOL/Old_Number_Theory/IntFact.thy	Sat Oct 10 16:26:23 2015 +0200
1.3 @@ -3,19 +3,19 @@
1.4      Copyright   2000  University of Cambridge
1.5  *)
1.6
1.7 -section {* Factorial on integers *}
1.8 +section \<open>Factorial on integers\<close>
1.9
1.10  theory IntFact
1.11  imports IntPrimes
1.12  begin
1.13
1.14 -text {*
1.15 +text \<open>
1.16    Factorial on integers and recursively defined set including all
1.17    Integers from @{text 2} up to @{text a}.  Plus definition of product
1.18    of finite set.
1.19
1.20    \bigskip
1.21 -*}
1.22 +\<close>
1.23
1.24  fun zfact :: "int => int"
1.25    where "zfact n = (if n \<le> 0 then 1 else n * zfact (n - 1))"
1.26 @@ -24,10 +24,10 @@
1.27    where "d22set a = (if 1 < a then insert a (d22set (a - 1)) else {})"
1.28
1.29
1.30 -text {*
1.31 +text \<open>
1.32    \medskip @{term d22set} --- recursively defined set including all
1.33    integers from @{text 2} up to @{text a}
1.34 -*}
1.35 +\<close>
1.36
1.37  declare d22set.simps [simp del]
1.38
```