Re: [isabelle] domintros generated by Function too weak



I have some more issues with the Function package, this time with the
domintros option.
[...]

I’m not sure if this is a bug in in the Function package, or an
unavoidable limitation.

It is an unavoidable limitation of the specific implementation, i.e., a bug. I know it for a long time, and it is (again) caused by some uncontrolled forward simplification (which is from the devil, but I didn't know how bad it was when I wrote the code). Maybe it is time for a new attempt of improving this... I'll have a look.

Alex





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