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