src/HOL/Auth/Message.thy
changeset 7057 b9ddbb925939
parent 6807 6737af18317e
child 9686 87b460d72e80
--- a/src/HOL/Auth/Message.thy	Wed Jul 21 15:20:26 1999 +0200
+++ b/src/HOL/Auth/Message.thy	Wed Jul 21 15:22:11 1999 +0200
@@ -28,36 +28,15 @@
 datatype  (*We allow any number of friendly agents*)
   agent = Server | Friend nat | Spy
 
-
-(*Datatype msg is (awkwardly) split into two parts to avoid having freeness
-  expressed using natural numbers.*)
-datatype  
-  atomic = AGENT  agent	(*Agent names*)
-         | NUMBER nat   (*Ordinary integers, timestamps, ...*)
-         | NONCE  nat   (*Unguessable nonces*)
-         | KEY    key   (*Crypto keys*)
-
 datatype
-     msg = Atomic atomic
+     msg = Agent  agent	    (*Agent names*)
+         | Number nat       (*Ordinary integers, timestamps, ...*)
+         | Nonce  nat       (*Unguessable nonces*)
+         | Key    key       (*Crypto keys*)
 	 | Hash   msg       (*Hashing*)
 	 | MPair  msg msg   (*Compound messages*)
 	 | Crypt  key msg   (*Encryption, public- or shared-key*)
 
-(*These translations complete the illustion that "msg" has seven constructors*)
-syntax
-  Agent       :: agent => msg
-  Number      :: nat   => msg
-  Nonce       :: nat   => msg
-  Key         :: key   => msg
-
-translations
-  "Agent x"   == "Atomic (AGENT x)"
-  "Number x"  == "Atomic (NUMBER x)"
-  "Nonce x"   == "Atomic (NONCE x)"
-  "Nonce``x"  == "Atomic `` (NONCE `` x)"
-  "Key x"     == "Atomic (KEY x)"
-  "Key``x"    == "Atomic `` (KEY `` x)"
-
 
 (*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)
 syntax