Re: [isabelle] Proof method to split disjunctions and conjunctions ?


Am Sonntag, den 08.12.2013, 01:01 +0100 schrieb Yannick Duchêne
> I obviously mean more or less long sequences of disjunctions and  
> conjunctions, not minimal “(?P ∨ ?Q)” or “(?P ∧ ?Q)”.

If you want to do in as the initial method of a Isar proof, I like to go
for something like
proof (elim conjE disjE, intro conjI)
(also see


Joachim “nomeata” Breitner
  mail at •
  Jabber: nomeata at  • GPG-Key: 0x4743206C
  Debian Developer: nomeata at

Attachment: signature.asc
Description: This is a digitally signed message part

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