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
*** 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
