Hi,
In the proof I have here, I took each instruction, and applied it in
sequence in the proof manager which worked. However the below doesn't
work. Is there something to the THEN tactical that I'm not
understanding?
Thanks!
(* prove |- (A ==> (B ==> ( A /\ B ))) in a backwards proof *)
val thm3 = prove( (--`(B ==> (A ==> ( A /\ B )))`--),
DISCH_TAC THEN
DISCH_TAC THEN
CONJ_TAC THEN
(UNDISCH_TAC (--`A:bool`--)) THEN
(ACCEPT_TAC ((DISCH_ALL (ASSUME (--`A:bool`--)))))THEN
(UNDISCH_TAC (--`B:bool`--)) THEN
(ACCEPT_TAC (DISCH_ALL (ASSUME (--`B:bool`--))))));
------------------------------------------------------------------------------
Enter the BlackBerry Developer Challenge
This is your chance to win up to $100,000 in prizes! For a limited time,
vendors submitting new applications to BlackBerry App World(TM) will have
the opportunity to enter the BlackBerry Developer Challenge. See full prize
details at: http://p.sf.net/sfu/Challenge
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
