replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style
(* 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