On Fri, 2008-10-03 at 14:14 +0200, Florian Haftmann wrote: > I also think that two would be better than three; technically > "undefined" is the same as "arbitrary"
Then what is the point of undefined_fun: "undefined x = undefined" in HOL.thy? Best, Tjark
