On Fri, 2013-02-15 at 13:37 +0100, Tobias Nipkow wrote:
* Sledgehammer spontaneously acts asynchronously of certain open
problems in the text, depending on certain parameters like time outs.
Triggering s/h via sorry (or some other explicit means) is perfectly
reasonable, but having
On Sunday, February 17, 2013 at 17:06:46 (+0100), Tjark Weber wrote:
On Fri, 2013-02-15 at 13:37 +0100, Tobias Nipkow wrote:
* Sledgehammer spontaneously acts asynchronously of certain open
problems in the text, depending on certain parameters like time outs.
Triggering
In private conversation, there has been some confusion concerning this
issue (stemming from the users mailinglist originally).
Let me clarify, quoting the tutorial on code generation:
--
Code_Binary_Nat implements type nat using a binary rather than a linear
representation, which yields a
Dear Larry, Stefan, Tobias, and Andrei (as authors of the relevant
Isabelle/HOL theories),
already several times I stumbled upon the definition of Relation.refl_on
(and thus also Order_Relation.Refl) and was irritated.
What is the reason for demanding r = A * A? And why are other
properties
Am 17/02/2013 19:41, schrieb Christian Urban:
On Sunday, February 17, 2013 at 17:06:46 (+0100), Tjark Weber wrote:
On Fri, 2013-02-15 at 13:37 +0100, Tobias Nipkow wrote:
* Sledgehammer spontaneously acts asynchronously of certain open
problems in the text, depending on
