On Thu, 27 May 2010, Florian Haftmann wrote:
It is possible to enter type variables distinguished only by sort
constraint on the Isar level:
lemma
assumes "P TYPE('a::order)" and "Q TYPE('a::group_add)"
shows "R TYPE('a::power)"
using assms proof -
It is not clear to me whether this his always been possible that way or
slipped in due to some change.
While this is OK for the low-level inference kernel, the syntax layer is
supposed to prevent such inconsistent constraints (both for type and term
variables).
The above is accepted even in Isabelle2005, and nobody has noticed so far.
When introducing the present check/uncheck infrastructure some years ago I
did notice some internal oddities concerning sort constraints that are
probably responsible for this effect. Some weeks ago I actually managed
to clear out some part of it (sort constraints for type specifications),
but did not get to the bottom of the whole syntax stack.
After the next round of check/uncheck modernization it should work in the
intended strict sense.
Makarius
_______________________________________________
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
