So, I have this..
- prove(--`B:bool`--,MP_TAC (ASSUME ``A:bool``) THEN ACCEPT_TAC
(mk_thm([],``A ==> B``)));
> val it = [A] |- B : thm
Which is fine and good,
but when I use the interactive prompt,
- g `B:bool`;
> val it =
Proof manager status: 1 proof.
1. Incomplete goalstack:
Initial goal:
B
: proofs
- e (MP_TAC (ASSUME ``A:bool``));
OK..
Exception raised at Tactical.VALID:
Invalid tactic
! Uncaught exception:
! HOL_ERR
-
I get this exception. The exception makes sense because the docs say
that the tactic isn't valid if the thm argument assumption list isn't a
subset of the goal assumption list. However if this is the case, then
why would the tactic work in the proof function?
Thanks,
-T.J.
------------------------------------------------------------------------------
The Windows 8 Center - In partnership with Sourceforge
Your idea - your app - 30 days.
Get started!
http://windows8center.sourceforge.net/
what-html-developers-need-to-know-about-coding-windows-8-metro-style-apps/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
