Re: [isabelle] Strange simplification



I think because it is parsed as

  (alls P ([] @ ys) = (alls P [])) \<and> (alls P ys)

when you want it to be interpreted as

  alls P ([] @ ys) = ((alls P []) \<and> (alls P ys))

Larry Paulson

On 8 Aug 2007, at 16:22, Cristiano Longo wrote:

I obtain two subgoals. The first is

alls P ([] @ ys) = (alls P []) \<and> (alls P ys)

I can't understand why, simplifier transform this goal to

alls P ys






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