Re: [isabelle-dev] Feedback from a Isabelle tutorial

2011-06-24 Thread Makarius
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

Re: [isabelle-dev] Sledgehammer

2011-06-24 Thread Clemens Ballarin
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

Re: [isabelle-dev] Sledgehammer

2011-06-24 Thread Jasmin Christian Blanchette
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

Re: [isabelle-dev] Feedback from a Isabelle tutorial

2011-06-24 Thread Alexander Krauss
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

[isabelle-dev] Sledgehammer

2011-06-24 Thread 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_Examples/Proxies.thy") I guess I lack some sort of heavy equip

Re: [isabelle-dev] Feedback from a Isabelle tutorial

2011-06-24 Thread Makarius
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

Re: [isabelle-dev] Feedback from a Isabelle tutorial

2011-06-24 Thread Christian Sternagel
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

Re: [isabelle-dev] Feedback from a Isabelle tutorial

2011-06-24 Thread Makarius
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

[isabelle-dev] Feedback from a Isabelle tutorial

2011-06-24 Thread Lukas Bulwahn
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