*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] what is the correct syntax to do simple auto prove proposition*From*: Gottfried Barrow <igbi at gmx.com>*Date*: Mon, 02 Jun 2014 13:20:28 -0500*In-reply-to*: <BAY178-W297E97D3F8F3364B1CCDECB6200@phx.gbl>*References*: <BAY178-W132669A0B0DF8D14AEAD6CB63B0@phx.gbl>, <922E7845-0465-44A0-9FCA-960F246D2ACE@gmail.com>, <BAY178-W4995ADD81CC57BEA2682E8B6200@phx.gbl> <BAY178-W297E97D3F8F3364B1CCDECB6200@phx.gbl>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

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

**References**:**Re: [isabelle] what is the correct syntax to do simple auto prove proposition***From:*Lee Martin CCNP

**Re: [isabelle] what is the correct syntax to do simple auto prove proposition***From:*Lee Martin CCNP

- Previous by Date: Re: [isabelle] what is the correct syntax to do simple auto prove proposition
- Next by Date: [isabelle] WST 2014: Call for Participation
- Previous by Thread: Re: [isabelle] what is the correct syntax to do simple auto prove proposition
- Next by Thread: Re: [isabelle] what is the correct syntax to do simple auto prove proposition
- Cl-isabelle-users June 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list