On Mon, 9 Jul 2012, Andreas Lochbihler wrote:
On the sister thread
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-July/msg00028.html
Henri mentions finite_UNIV.
Henri refers to finite_UNIV in HOL/Finite_Set, you seem to talk about
finite_UNIV from HOL/Library/Cardinality.
I did not look that closely, merely spending 5min on his example, to see a
difference in the theorem statements in Isabelle2012 vs.
Isabelle/3155cee13c49. Maybe part of the confusion is a wrong import. (I
am presently on a conference, so nothing new will come from my side for
this mysterious blast incident of Henri.)
The first hit in Google when you search for "phantom type" tells you
what a phantom type is. "A phantom type is a type whose type parameter
do not all appear on the right-hand side of it's defintion."
[http://www.haskell.org/haskellwiki/Phantom_type]
As can be seen from the usage of Phantom('a) in Cardinality
(e97369f20c30 and 3d9c1ddb9f47) and the commit message in e97369f20c30,
phantom types can be used to make a type parameter appear in a
constant's type.
So far this is about Haskell, not Isabelle. So no relevant information
for NEWS.
Typically in Isabelle, such constants take an additional argument 'a
itself for that purpose, but this generates less efficient code than
boxing values in phantom types of which the ML/Haskell compiler gets rid
again.
The last paragraph looks like the missing information for NEWS. It
explains why the known Isabelle solution was not used here. (And I can't
say anything myself about if and how it could actually impact code
generation.)
Generally, NEWS tells about the "user-relevant changes" for official
releases, but it usually saves a lot of time to update that ealier, e.g. 2
days .. 2 weeks after the actual change.
Log entries are also an opportunity to justify what was done and why, in
less than half a sentence. There is a special art and virtuosity of
formal shorthand writing. The message is meant for the anonymous
Mercurial historian studying the log 2 days or 2 years later.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
