Re: [isabelle] defining nat1 in isabelle
Am 16.04.2013 um 15:02 schrieb Stephan van Staden <Stephan.vanStaden at inf.ethz.ch>:
> I think this use of "typedef" is deprecated. Although Isabelle still accepts it, I remember seeing warnings.
"Typedef" is still as encouraged as ever (modulo Tobias's warnings about the lack of automation). The warnings were probably tied to a specific usage of typedef. This is from the "NEWS" file:
* Simplified 'typedef' specifications: historical options for implicit
set definition and alternative name have been discontinued. The
former behavior of "typedef (open) t = A" is now the default, but
written just "typedef t = A". INCOMPATIBILITY, need to adapt theories
If I recall right, during the transition period, "typedef" without "open" used to generate a warning.
This archive was generated by a fusion of
Pipermail (Mailman edition) and