Re: [Hol-developers] PSL proof fails

[Joe H. <joe...@co...>]

I'm in the middle of reworking these lemmas, so I'm quite prepared to
believe that one or more of them is currently broken. If future errors
appear in ExecuteSemanticsScript before I've checked in a version that
definitely says "it now works" then don't worry about it.

Joe

On Thu, 23 Oct 2003, Michael Norrish wrote:

> I realised that I hadn't checked my latest change (yesterday's change
> to the simplifier's mk_rewrites code) against the PSL example.  I've
> just done this this morning, and it fails to prove a lemma
>
>   boolean_safety_violation
>
> in ExecutableSemanticsScript.sml.
>
> I don't think this failure is my fault though because the same error
> arises when I try to run the example through a version of HOL without
> the change to mk_rewrites in place.
>
> Of course, it may well be that the error arises because of some
> earlier change I made to the system.  I will endeavour to check all
> the examples when I make any future changes.  (This is relatively easy
> to do using the build_examples script from <holdir>/developers/ )
>
> Michael.
>
>
>
>
>
>
>
> -------------------------------------------------------
> This SF.net email is sponsored by OSDN developer relations
> Here's your chance to show off your extensive product knowledge
> We want to know what you know. Tell us and you have a chance to win $100
> http://www.zoomerang.com/survey.zgi?HRPT1X3RYQNC5V4MLNSV3E54
> _______________________________________________
> Hol-developers mailing list
> Hol...@li...
> https://lists.sourceforge.net/lists/listinfo/hol-developers
>