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



Hi,

Am Sonntag, den 08.12.2013, 01:01 +0100 schrieb Yannick Duchêne
(Hibou57):
> 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 http://stackoverflow.com/a/15901571/946226)

Greetings,
Joachim

-- 
Joachim “nomeata” Breitner
  mail at joachim-breitner.de • http://www.joachim-breitner.de/
  Jabber: nomeata at joachim-breitner.de  • GPG-Key: 0x4743206C
  Debian Developer: nomeata at debian.org

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



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