Re: [isabelle] what is the correct syntax to do simple auto prove proposition



On 14-06-02 06:05, Lee Martin CCNP wrote:
> here is the link, how current situation is.
> https://drive.google.com/file/d/0Bxs_ao6uuBDUcjE0RUxtNEEwajA/edit?usp=sharing
Lee,

You're leaving your filename as the default, "Scratch.thy", but you have
"theory Foo". The filename must be the same as the theory name. Change
your filename to Foo.thy, or change your theory to Scratch.

The error messages will give you feedback that can help you figure
things out. In this case, the error message is this: "Bad file name
"Scratch.thy" for theory "Foo".

It's displayed in the output panel, or it's displayed if you place your
mouse cursor over "theory," with the red line underneath it.

Regards,
GB



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.