src/HOL/Library/Stirling.thy
changeset 63145 703edebd1d92
parent 63071 3ca3bc795908
child 63487 6e29fb72e659
     1.1 --- a/src/HOL/Library/Stirling.thy	Tue May 24 22:46:23 2016 +0200
     1.2 +++ b/src/HOL/Library/Stirling.thy	Wed May 25 11:49:40 2016 +0200
     1.3 @@ -1,13 +1,13 @@
     1.4  (* Authors: Amine Chaieb & Florian Haftmann, TU Muenchen
     1.5              with contributions by Lukas Bulwahn and Manuel Eberl*)
     1.6  
     1.7 -section {* Stirling numbers of first and second kind *}
     1.8 +section \<open>Stirling numbers of first and second kind\<close>
     1.9  
    1.10  theory Stirling
    1.11  imports Binomial
    1.12  begin
    1.13  
    1.14 -subsection {* Stirling numbers of the second kind *}
    1.15 +subsection \<open>Stirling numbers of the second kind\<close>
    1.16  
    1.17  fun Stirling :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    1.18  where
    1.19 @@ -54,7 +54,7 @@
    1.20    "Stirling (Suc n) (Suc (Suc 0)) = 2 ^ n - 1"
    1.21    using Stirling_2_2 by (cases n) simp_all
    1.22  
    1.23 -subsection {* Stirling numbers of the first kind *}
    1.24 +subsection \<open>Stirling numbers of the first kind\<close>
    1.25  
    1.26  fun stirling :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    1.27  where