Re: [isabelle] Strange simplification



Hi Christiano,

[...]
and tried to prove the following lemma
alls P (xs @  ys) = (alls P xs)  \<and> (alls P ys)

What you see is not what you mean(tm): Equality binds stronger than conjunction, so you are actually proving

(alls P (xs @  ys) = alls P xs)  \<and> (alls P ys)

instead of

alls P (xs @  ys) = (alls P xs  \<and> alls P ys) .

Hence the "strange" behaviour.

Alex





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