[isabelle-dev] Fwd: [isabelle] Pending sort hypotheses
makarius at sketis.net
Mon Jul 9 23:14:28 CEST 2012
On Mon, 9 Jul 2012, Andreas Lochbihler wrote:
>> On the sister thread
>> 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."
> 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
> 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
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
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.
More information about the isabelle-dev