Email Gateway (Aug 19 2022 at 14:33): Email Gateway (Aug 19 2022 at 14:33):From: Lee Martin CCNP <tesleft@hotmail.com>
Hi sir,
After choose sledgerhammer, and check isar proof and click Apply, got error
what is the correct syntax to prove simple proposition
Illegal application of command "lemma" at top level
lemma "(a ∨ b) ∧ (b ∨ c) --> (a ∨ c)"apply autodone
Regards,
Martin
Email Gateway (Aug 19 2022 at 14:33):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Martin,
Is this your entire theory file? If so, you will need to start with the usual header. Assuming your theory file is called Foo.thy, this means:
theory Foo
imports Main
begin
This should be explained in the tutorials (the first two bullet points at http://isabelle.in.tum.de/documentation.html).
Regards,
Jasmin
Email Gateway (Aug 19 2022 at 14:34):From: Lee Martin CCNP <tesleft@hotmail.com>
Hi Jasmin,
in window 8, i open Isabelle2013-2.exe
it return error
[line 1 of "$ISABELLE_HOME_USER/etc/preferences"] error: bad input
ini file do not have this path
then i open cygwin-terminal.bat and click Isabelle2013-2.exe again, still got error
in cygwin-terminal.bat i type ./Isabelle2013-2.exe got the same error too.
Regards,Martin
Email Gateway (Aug 19 2022 at 14:34):From: Makarius <makarius@sketis.net>
It is hard to guess from a distance. Maybe something is just wrong with
your local Isabelle installation.
When you start the main exe, do you get the Isabelle/jEdit application
with the prover running, and giving feedback on your theory? You can try
that quickly by the Documentation panel, with the Examples at the bottom.
There should be some flashing of colors when you open src/HOL/ex/Seq.thy
for example.
Moreover, can you say what this produces in the Output window?
ML {* getenv "USER_HOME"; getenv "ISABELLE_HOME"; getenv "ISABELLE_HOME_USER" *}
Again this needs to be a proper theory file with theory header, e.g. the
body of one of the examples (without saving the changed file).
Makarius
Email Gateway (Aug 19 2022 at 14:34):From: Lee Martin CCNP <tesleft@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?
Regards,
Martin
Email Gateway (Aug 19 2022 at 14:40):From: Lee Martin CCNP <tesleft@hotmail.com>
Hi Jasmin,
here is the link, how current situation is.
https://drive.google.com/file/d/0Bxs_ao6uuBDUcjE0RUxtNEEwajA/edit?usp=sharing
Regards,
Martin
Email Gateway (Aug 19 2022 at 14:42):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Dear Martin,
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
Email Gateway (Aug 19 2022 at 14:45):From: Gottfried Barrow <igbi@gmx.com>
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
Last updated: Apr 18 2024 at 16:19 UTC