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

2011-06-25 Thread Makarius
On Sat, 25 Jun 2011, Clemens Ballarin wrote: Quoting Makarius : In principle everything is possible, but one needs to try hard to minimize "options" and "features". Otherwise it becomes impossible to maintain robustness of the application. There are no proper automated test procedures, whi

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

2011-06-25 Thread Clemens Ballarin
Quoting Makarius : In principle everything is possible, but one needs to try hard to minimize "options" and "features". Otherwise it becomes impossible to maintain robustness of the application. There are no proper automated test procedures, which means I usually play through all the im

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

2011-06-25 Thread Makarius
On Sat, 25 Jun 2011, Lawrence Paulson wrote: Is it possible to restrict command completion to a select collection of commonly used commands? Or to make it the user-configurable? Larry On 24 Jun 2011, at 21:01, Alexander Krauss wrote: Suggestion: Simply kill completion of commands (not symbol

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

2011-06-25 Thread Lawrence Paulson
Is it possible to restrict command completion to a select collection of commonly used commands? Or to make it the user-configurable? Larry On 24 Jun 2011, at 21:01, Alexander Krauss wrote: > Suggestion: Simply kill completion of commands (not symbols)???

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

2011-06-25 Thread Makarius
On Fri, 24 Jun 2011, Alexander Krauss wrote: Another instance, which comes up in an exploratory/teaching context, is the following scenario: lemma "x = y"-- some false conjecture try -- see if it "works" ^ -> counterexample found immediately cur