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.

Cheers,
Gerwin





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