[isabelle] abbreviated the MPair



Dear All

I would to do that:

the notation {X ,Y} abbreviates MPair X Y

which I have define MPiar as type of message as follow

datatype message =
                          MPair message message.

what is the best way to do it. I have tried to do it by translations but is
not work as


datatype message =
                         MPair message message.

translations
"{X,Y}" <=> "MPair X Y"

Best Regards,




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