[isabelle-dev] Datatype alt_names

[Makarius]

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.


 	Makarius