Re: [isabelle] Automatic pair splitting by auto

Hi Peter,

someone once told me this ML command:

declare split_paired_All [simp del] split_paired_Ex [simp del]
ML_setup {*
change_simpset (fn ss => ss delloop "split_all_tac");
change_claset (fn cs => cs delSWrapper "split_all_tac");

to turn pair splitting off and

declare split_paired_All [simp] split_paired_Ex [simp]
ML_setup {*
change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));

to turn it on again. Worked fine for me.


> 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.