Re: [isabelle] intro rule for &&&



Hi,

Am Donnerstag, den 20.12.2012, 12:02 +0100 schrieb John Wickerson:
> When I type...
> 
> > lemma assumes "A ∧ B" shows "A" "B"
> > using assms
> > apply rule

I was told, but don’t understand the reasons, that this works as an
intro rule for &&&:

lemma assumes "A ∧ B" shows "A" "B"
using assms
apply -

goal (2 subgoals):
 1. A ∧ B ⟹ A
 2. A ∧ B ⟹ B 


But I’m also looking forward for pedagogical enlightenment. 

Greetings,
Joachim
-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.info.uni-karlsruhe.de/~breitner

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



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