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
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
