[isabelle-dev] Datatype alt_names

Makarius makarius at sketis.net
Fri Nov 5 16:03:14 CET 2010

On Wed, 3 Nov 2010, Makarius wrote:

> On Wed, 3 Nov 2010, Brian Huffman wrote:
>> Consider this typedef command from an old version of HOLCF:
>> typedef (Sprod)  ('a, 'b) "**" (infixr 20) = "{f. ? a b. f = Spair_Rep
>> (a::'a) (b::'b)}"
>> The name "Sprod" sets "Rep_Sprod" and "Abs_Sprod" as the default names
>> for the morphisms (which could just as well be done with the
>> "morphisms" option). It also gives the name "Sprod" to the defined
>> set, and causes the generated theorem names to be qualified with
>> "Sprod".
>> I am guessing that the original motivation for this feature is the same as 
>> the reason for the similar feature in the datatype package: to support 
>> non-alphanumeric type names like "**".
> OK, there is yet another reason for that ancient alternative name. 
> Before the typedef package existed, Larry had a certain standard scheme 
> to write the axioms by hand, but the names where derived from a 
> capitalized version of the later type name.  This option allowed to 
> imitate Larry's old scheme and thus helped to save many hours or many 
> days of recompiling existing theories after name changes as we would do 
> now.

I did not find time yet to investigate the sources/history further, but I 
have just attended a talk where the presenter was using 'typedef' with 
this alternative name.  So its probably better not to delete it without a 
strong reason.


More information about the isabelle-dev mailing list