(* factorial n = m

   Invariant:
   If n >= 0 then m = n!
*)

fun factorial 0 = 1
  | factorial n = n * factorial (n-1)