Jasmin Blanchette wrote:
This motivates me to attack the "linarith" problem. If nobody
objects, I'll call the property "linarith_verbose" and have it on by
default (for compatibility) but off in "try_methods" and "try". I've
also taken the liberty to reword the "counterexample trace" message
>> you get the warning
>>
>> ### Metis: Unused theorems: "List.map.simps_2"
>>
>> which is strange because in Metis's code that warning is only printed if
>> "verbose" is true. Is "Proof.map_context" not the thing I should be using?
>
> Proof.map_context is right, also the use of the context
On Sun, 26 Jun 2011, Jasmin Christian Blanchette wrote:
Now, this all sounds well and good, but there is a little glitch. In
"try_methods.ML" the line
val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose
false)
is meant to tell Metis to be quiet, but somehow it is ignored.
Am 24.06.2011 um 11:32 schrieb Lukas Bulwahn:
> I only noticed that using "try" you often get a misleading response from
> linarith that "linarith found a counterexample" which beginners might stumble
> on.
> It might be better to switch off this warning by default (and offer a
> configuration
Command completion needs to be context aware to work well. Otherwise it
can indeed become a distraction.
Tobias
Am 24/06/2011 22:01, schrieb 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/p
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
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
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
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)???
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
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 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
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
16 matches
Mail list logo
