src/HOL/Analysis/Gamma_Function.thy
changeset 66453 cc19f7ca2ed6
parent 66447 a1f5c5c26fa6
child 66512 89b6455b63b6
equal deleted inserted replaced
66452:450cefec7c11 66453:cc19f7ca2ed6
     7 theory Gamma_Function
     7 theory Gamma_Function
     8 imports
     8 imports
     9   Conformal_Mappings
     9   Conformal_Mappings
    10   Summation_Tests
    10   Summation_Tests
    11   Harmonic_Numbers
    11   Harmonic_Numbers
    12   "~~/src/HOL/Library/Nonpos_Ints"
    12   "HOL-Library.Nonpos_Ints"
    13   "~~/src/HOL/Library/Periodic_Fun"
    13   "HOL-Library.Periodic_Fun"
    14 begin
    14 begin
    15 
    15 
    16 text \<open>
    16 text \<open>
    17   Several equivalent definitions of the Gamma function and its
    17   Several equivalent definitions of the Gamma function and its
    18   most important properties. Also contains the definition and some properties
    18   most important properties. Also contains the definition and some properties