--- a/src/HOL/SET_Protocol/Message_SET.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/SET_Protocol/Message_SET.thy Thu Sep 11 19:32:36 2014 +0200
@@ -52,11 +52,11 @@
text{*Agents. We allow any number of certification authorities, cardholders
merchants, and payment gateways.*}
-datatype_new
+datatype
agent = CA nat | Cardholder nat | Merchant nat | PG nat | Spy
text{*Messages*}
-datatype_new
+datatype
msg = Agent agent --{*Agent names*}
| Number nat --{*Ordinary integers, timestamps, ...*}
| Nonce nat --{*Unguessable nonces*}