>> 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? > > It’s simple: the prove function doesn’t perform the tactic-validity test. > > Tactic-validity is explicitly checked by the e function; most other > tools don’t bother. The validity test can be a useful guard against > errors, but these are most likely to occur as you interactively > develop a proof. By the time you come to execute a proof, it’s > assumed you know what you’re doing, and that your tactic really does > prove the theorem you think it does. > > Michael Has an error ever shown up because of this validity test not being checked in every case the tactic is ran?
------------------------------------------------------------------------------ Everyone hates slow websites. So do we. Make your web apps faster with AppDynamics Download AppDynamics Lite for free today: http://p.sf.net/sfu/appdyn_sfd2d_oct _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
