src/HOL/Old_Number_Theory/IntFact.thy
changeset 63167 0909deb8059b
parent 61382 efac889fccbc
     1.1 --- a/src/HOL/Old_Number_Theory/IntFact.thy	Thu May 26 16:57:14 2016 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/IntFact.thy	Thu May 26 17:51:22 2016 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  
     1.5  text \<open>
     1.6    Factorial on integers and recursively defined set including all
     1.7 -  Integers from @{text 2} up to @{text a}.  Plus definition of product
     1.8 +  Integers from \<open>2\<close> up to \<open>a\<close>.  Plus definition of product
     1.9    of finite set.
    1.10  
    1.11    \bigskip
    1.12 @@ -26,7 +26,7 @@
    1.13  
    1.14  text \<open>
    1.15    \medskip @{term d22set} --- recursively defined set including all
    1.16 -  integers from @{text 2} up to @{text a}
    1.17 +  integers from \<open>2\<close> up to \<open>a\<close>
    1.18  \<close>
    1.19  
    1.20  declare d22set.simps [simp del]