src/HOL/Hyperreal/Fact.thy
changeset 15131 c69542757a4d
parent 15094 a7d1a3fdc30d
child 15140 322485b816ac
equal deleted inserted replaced
15130:dc6be28d7f4e 15131:c69542757a4d
     4     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     4     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     5 *)
     5 *)
     6 
     6 
     7 header{*Factorial Function*}
     7 header{*Factorial Function*}
     8 
     8 
     9 theory Fact = Real:
     9 theory Fact
       
    10 import Real
       
    11 begin
    10 
    12 
    11 consts fact :: "nat => nat"
    13 consts fact :: "nat => nat"
    12 primrec
    14 primrec
    13    fact_0:     "fact 0 = 1"
    15    fact_0:     "fact 0 = 1"
    14    fact_Suc:   "fact (Suc n) = (Suc n) * fact n"
    16    fact_Suc:   "fact (Suc n) = (Suc n) * fact n"