Re: [isabelle] recdef woes
On Friday 02 December 2005 17:06, Michael Norrish wrote:
> Alexander Krauss writes:
> > If you were using "list_all" instead, a similar rule for list_all would
> > be needed. The reason that it works out of the box when you use "map"
> > is simply that a congruence rule is included by default.
> I still don't understand why list_all on its own didn't work, but
> when I combined list_all with map it did work. Anyway, thanks for the
> help in finding a workaround.
I just checked the library: that is because there is a congruence rule for
map, but none for list_all.
In the example with "list_all id (map ..)" the "id" probably made it simple
enough to deal with.
This archive was generated by a fusion of
Pipermail (Mailman edition) and