On Fri, 24 Jun 2011, Alexander Krauss wrote:
It is a known issue (if an issue at all) that in Isabelle/jEdit it is
sometimes necessary to cut-and-paste some lines in order to
"synchronize."
This behaviour is indeed getting in the way in practice. It works
according to the "specification" of
Hi Jasmin,
Thanks for this hint. It turns out that I had set E_HOME to some
bogus location. Residue of some old setup... Now it work fine.
Clemens
Quoting Jasmin Christian Blanchette :
Am 24.06.2011 um 20:13 schrieb Clemens Ballarin:
While doing an 'isabelle makeall all' on my local m
Am 24.06.2011 um 20:13 schrieb Clemens Ballarin:
> While doing an 'isabelle makeall all' on my local machine, I encountered the
> error
>
> Sledgehammering...
> *** Unexpected outcome: "unknown".
> *** At command "sledgehammer" (line 26 of
> "/Users/ballarin/isabelle/hg/src/HOL/Metis_Example
Hi all,
Now that this topic is already active, here is more:
In a small course here at TUM
(http://www4.in.tum.de/lehre/vorlesungen/perlen/SS11/) we are also using
jedit exclusively for the first time, and I can confirm the observation
that it makes it slightly easier for newbies to get start
While doing an 'isabelle makeall all' on my local machine, I
encountered the error
Sledgehammering...
*** Unexpected outcome: "unknown".
*** At command "sledgehammer" (line 26 of
"/Users/ballarin/isabelle/hg/src/HOL/Metis_Examples/Proxies.thy")
I guess I lack some sort of heavy equip
On Fri, 24 Jun 2011, Christian Sternagel wrote:
It is a known issue (if an issue at all) that in Isabelle/jEdit it is
sometimes necessary to cut-and-paste some lines in order to
"synchronize." Some students found this unexpected or even weren't able
to solve exercises in the beginning since th
On 06/24/2011 01:37 PM, Makarius wrote:
On Fri, 24 Jun 2011, Lukas Bulwahn wrote:
Johannes Hoelzl and me, gave a two-and-half-hour tutorial to Isabelle
at a workshop meeting of PhD students in computer science in Dagstuhl
(cf. http://www.model.in.tum.de/um/vernetzungstreffen/).
Thanks for the
On Fri, 24 Jun 2011, Lukas Bulwahn wrote:
Johannes Hoelzl and me, gave a two-and-half-hour tutorial to Isabelle at
a workshop meeting of PhD students in computer science in Dagstuhl (cf.
http://www.model.in.tum.de/um/vernetzungstreffen/).
Thanks for the feedback. I would like to add the page
Hello all,
this week, we, Johannes Hoelzl and me, gave a two-and-half-hour tutorial
to Isabelle at a workshop meeting of PhD students in computer science in
Dagstuhl (cf. http://www.model.in.tum.de/um/vernetzungstreffen/).
We used Isabelle/jEdit with some latest development snapshot and bun
