[isabelle-dev] An ARBITRARY question

Tjark Weber tjark.weber at gmx.de
Fri Oct 3 16:25:52 CEST 2008


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




More information about the isabelle-dev mailing list