[isabelle-dev] Datatype alt_names

[Makarius]

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.


 	Makarius