On Mi, 2012-10-17 at 11:09 +0200, Makarius wrote:
*** ML ***
* Type Seq.results and related operations support embedded error
messages within lazy enumerations, and thus allow to provide
informative errors in the absence of any usable results.
Cool, no more writing of error messages to the
On Wed, 17 Oct 2012, Peter Lammich wrote:
On Mi, 2012-10-17 at 11:09 +0200, Makarius wrote:
*** ML ***
* Type Seq.results and related operations support embedded error
messages within lazy enumerations, and thus allow to provide
informative errors in the absence of any usable results.
Cool,
In jedit, numerals of polymorphic type are no longer tagged with the type
variable as a warning. That is an extremely helpful warning not just for
beginners, it would be a pity to lose that in jedit.
Tobias
___
isabelle-dev mailing list
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}
