Re: [isabelle] Warning for partial functions defined with fun?



Hi Thomas,

great! I remember about this discussion but did not imagine that it was
already added to Isabelle :-)

The relevant changeset is here:

http://isabelle.in.tum.de/repos/isabelle/rev/fcb6250bf6b4

Do you know if I can apply a particular changeset to my Isabelle2011 or
have to get the full developpement version?

This one is simple enough, and there haven't been much changes, so it should probably work if you just apply this change (click on "raw" at the URL above to get the actual patch) and recompile HOL using "./build".

In general, this almost never works, due to interactions with other changes, but here you may be lucky.

Alex





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.