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