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.
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
