[isabelle-dev] Fwd: [isabelle] Pending sort hypotheses

[Makarius]

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