[isabelle] Automatic pair splitting by auto



Hi all,

How can I tell the auto-method NOT to do pair splitting automatically?
E.g. having

consts P::"'a*'a => bool"

lemma test: "!!a. P a \<and> (True --> True)"
  apply auto

gives
  "!!a b. P (a,b)"

but I need:
  !!a. P a

regards and thanks in advance,
  Peter

p.s. I could have used simp for this particular example, but for my actual task, I need auto.







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