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:

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.


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