Re: [isabelle] recdef woes
The following congruence rule for bounded universial quantification solves your
"[| M = M'; !!x. x : M ==> P x = P' x |]
==> (ALL x: M. P x) = (ALL x: M'. P' x)"
After this, recdef behaves nicely.
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.
Hope this helps
This archive was generated by a fusion of
Pipermail (Mailman edition) and