On Tue, Oct 30, 2012 at 6:44 PM, Konrad Slind <[email protected]>wrote:
> > Ok, so if I understand this correctly the validity checks are only in
> > place to keep you from going down an inference chain that is guarenteed
> > to go no where in making progress towards proving your goal. This being
> > only an issue when searching for the proof itself in the interactive
> > prompt, not when just verifying it.
>
>
> The way I think about it is that the validity check makes sure that no
> assumptions beyond those stated in the goal enter the proof. For some
> applications, adding new assumptions might be just the trick, e.g., when
> exploring a proof to see what assumptions are needed. In that case,
> expandf is your friend.
>
Pardon me, what is expandf? I don't see it mentioned in the HOL Light
documentation, for what that is worth.
-Cris
> Konrad.
>
>
> ------------------------------------------------------------------------------
> 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
>
------------------------------------------------------------------------------
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
