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> wrote:

I suggest “safe” or “clarify”.

Larry Paulson


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!

--
Yannick Duchêne




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