reimplementation of HOL records; only one type is created for
each record extension, instead of one type for each field. See NEWS.
(* Title : Fact.thy
Author : Jacques D. Fleuriot
Copyright : 1998 University of Cambridge
Description : Factorial function
*)
Fact = NatStar +
consts fact :: nat => nat
primrec
fact_0 "fact 0 = 1"
fact_Suc "fact (Suc n) = (Suc n) * fact n"
end