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.


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