src/HOL/Hyperreal/Fact.thy
changeset 12196 a3be6b3a9c0b
child 15094 a7d1a3fdc30d
equal deleted inserted replaced
12195:ed2893765a08 12196:a3be6b3a9c0b
       
     1 (*  Title       : Fact.thy 
       
     2     Author      : Jacques D. Fleuriot
       
     3     Copyright   : 1998  University of Cambridge
       
     4     Description : Factorial function
       
     5 *)
       
     6 
       
     7 Fact = NatStar + 
       
     8 
       
     9 consts fact :: nat => nat 
       
    10 primrec 
       
    11    fact_0     "fact 0 = 1"
       
    12    fact_Suc   "fact (Suc n) = (Suc n) * fact n" 
       
    13 
       
    14 end