On 10/19/2012 04:35 PM, Makarius wrote:
On Fri, 19 Oct 2012, Lukas Bulwahn wrote:
Operations like Simplifier.context, Simplifier.inherit_context
should help here. Once that is repaired, I will see if the warning
can now be made an error that is more explicit about the reasons.
I am
On Wed, 17 Oct 2012, Lukas Bulwahn wrote:
If you update to changeset 89b118c0c070, the issue should be resolved.
There still seem to be remaining issues: Isabelle/d1ecb3554b25 and
AFP/15527cc14202:
Girth_Chromatic FAILED
(see also
On Fri, 19 Oct 2012, Lukas Bulwahn wrote:
Operations like Simplifier.context, Simplifier.inherit_context should
help here. Once that is repaired, I will see if the warning can now be
made an error that is more explicit about the reasons.
I am certainly in favour of this. First, tool
Hi Dmitriy,
If you update to changeset 89b118c0c070, the issue should be resolved.
Lukas
On 10/16/2012 01:41 PM, Dmitriy Traytel wrote:
Hi all,
the following produces a Loose bound variable with
Isabelle/4a15873c4ec9
theory Scratch
imports Main
begin
lemma finite {y |y. ∃x. y ∈ f x}
Hi all,
the following produces a Loose bound variable with Isabelle/4a15873c4ec9
theory Scratch
imports Main
begin
lemma finite {y |y. ∃x. y ∈ f x}
apply simp
oops
end
Fortunately, jedit treats a proof that used to work (but fails now due
to the above) as a sorry, such that I can continue
