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
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
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
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
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 equipment
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
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
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 jasmin.blanche...@gmail.com:
Am 24.06.2011 um 20:13 schrieb Clemens Ballarin:
While doing an
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 the
