Mixfix annotations have gained a more formal status recently, with PIDE
markup reports that lead to some highlighting and tooltips in the IDE.
In order to make this work cleanly, there needs to be exactly one
"interning" of the input given by the user. E.g. for the term language
this is done
> In Isabelle/cfbb6a5b427c it is done again differently, and hopefully in
> a more robust way.
Thanks, that seems to have resolved the matter.
Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
On Tue, 12 Apr 2016, Lawrence Paulson wrote:
A relevant past message.
We have more messages in the archives, about blast ignoring the
distinction of Trueprop vs. non-Trueprop propositions. This boils down to
the following example, which is non-terminating in Isabelle2016 and
current
On Tue, 12 Apr 2016, Peter Lammich wrote:
so we're not going to see the annoying "... not of sort 'type'" error
any more, which used to occur occasionally in Isabelle/HOL
developments!?
Yes, but old tools may get broken, if slightly more general types are
expected. E.g. see the record
Nice one,
so we're not going to see the annoying "... not of sort 'type'" error
any more, which used to occur occasionally in Isabelle/HOL
developments!?
--
Peter
On Di, 2016-04-12 at 16:46 +0200, Makarius wrote:
> *** General ***
>
> * Type-inference improves sorts of newly introduced type
On Mon, 11 Apr 2016, Lars Hupel wrote:
I wanted to try out some of the changes you made in the past week, but
unfortunately, I'm getting exceptions upon starting Isabelle/jEdit.
12:33:24 [main] [error] Plugin: java.lang.ExceptionInInitializerError
Odd. I don't see this problem on my
*** General ***
* Type-inference improves sorts of newly introduced type variables for
the object-logic, using its base sort (i.e. HOL.type for Isabelle/HOL).
Thus terms like "f x" or "⋀x. P x" without any further syntactic context
produce x::'a::type in HOL instead of x::'a::{} in Pure. Rare
A relevant past message.
Larry
> Begin forwarded message:
>
> From: Makarius
> Subject: Re: [isabelle] TERM exception in fologic.ML
> Date: 27 October 2014 at 20:22:02 GMT
> To: Slawomir Kolodynski
> Cc: "cl-isabelle-us...@lists.cam.ac.uk"
I wonder if we can look at this problem, which has been around for at least 18
months. It seems to be connected with the recent modification to hyp_subst_tac,
which now retains the equality. (The workaround of switching off this behaviour
is not a true solution.) I took a look at this code