Re: [isabelle] Proof method to split disjunctions and conjunctions ?
On Sun, 08 Dec 2013 01:13:09 +0100, Lawrence Paulson <lp15 at cam.ac.uk>
I suggest “safe” or “clarify”.
I will try those two right after. I was back to ask the same with things
like “show "⟦?H0; ?H1; ?H2⟧ ⟹ ?thesis"”, I mean if there is a method to
choose to prove it by proving "¬ ?H0".
I'm looking at “safe” or “clarify” in Isar‑Ref right in a minute (I need
to understand what it precisely do, … don't want to just play with it).
Lot of thanks for the pointers Larry!
This archive was generated by a fusion of
Pipermail (Mailman edition) and