[isabelle] datatype display problem of type_synonym



Hi,

I tried the following:

type_synonym my_int = int

   text {* @{typ my_int} *}

   datatype foo = A | B my_int

   text {* @{datatype foo} *}

The "text" works and prints out "my_int",
but the "datatype" prints out "int"
which should be "my_int".

Is there an attribute for datatype antiquotation
to solve this problem?

Regards,

Chunhan




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.