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