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



Dear Martin,

Am 02.06.2014 um 13:04 schrieb Lee Martin CCNP <tesleft at hotmail.com>:

> Hi Jasmin,
> 
> after try in ubuntu, and press apply , it is like loading, no output or response show.
> 
> How to use it correctly?

The fact that I answered your first question should not be taken to mean that I will be responsible for answering all your questions from now on. Different Isabelle developers are responsible for different aspects of the system. Hence, I recommend that you address your queries to the entire mailing list, thereby letting the most appopriate developer or fellow user answer the request.

Judging from your video, I believe you are fighting with the basic interaction model of Isabelle/jEdit. I notice a red exclamation mark next to the keyword "theory", which suggests that the theory "Main" is not loaded. Try saving the file; usually this is enough to trigger some logic in Isabelle/jEdit that reloads background theories.

Regards,

Jasmin




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