On 30/10/12 13:18, Tony Johnson wrote: >> It’s simple: the prove function doesn’t perform the tactic-validity test.
[..] > Has an error ever shown up because of this validity test not being checked in > every case the tactic is ran? I can’t think of an instance, no. But, what do you mean by “error”? The basic LCF design means that soundness errors cannot occur because of this check being omitted. In particular, tactic-validity has nothing to do with the soundness of the kernel’s inferences. Michael ------------------------------------------------------------------------------ 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
