# HG changeset patch
# User paulson
# Date 902133454 -7200
# Node ID 701fa0ed77b7bd764707724074fea1fa1653bfca
# Parent  3571ff68cedab71aa73a03a4f24e3d3af3a4476d
Better comments

diff -r 3571ff68ceda -r 701fa0ed77b7 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Mon Aug 03 10:36:39 1998 +0200
+++ b/src/HOL/Auth/Message.thy	Mon Aug 03 10:37:34 1998 +0200
@@ -31,6 +31,9 @@
 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, ...*)
@@ -38,26 +41,31 @@
          | KEY    key   (*Crypto keys*)
 
 datatype
-  msg = Atomic atomic
-      | Hash   msg       (*Hashing*)
-      | MPair  msg msg   (*Compound messages*)
-      | Crypt  key msg   (*Encryption, public- or shared-key*)
+     msg = Atomic atomic
+	 | Hash   msg       (*Hashing*)
+	 | MPair  msg msg   (*Compound messages*)
+	 | Crypt  key msg   (*Encryption, public- or shared-key*)
 
-(*Allows messages of the form {|A,B,NA|}, etc...*)
+(*These translations complete the illustion that "msg" has seven constructors*)
 syntax
-  Agent          :: agent => msg
-  Number         :: nat   => msg
-  Nonce          :: nat   => msg
-  Key            :: key   => msg
+  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)"
+  "Key x"     == "Atomic (KEY x)"
+  "Key``x"    == "Atomic `` (KEY `` x)"
+
+
+(*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)
+syntax
   "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
 
 translations
-  "Agent x"       == "Atomic (AGENT x)"
-  "Number x"	  == "Atomic (NUMBER x)"
-  "Nonce x"	  == "Atomic (NONCE x)"
-  "Key x"	  == "Atomic (KEY x)"
-  "Key``x"	  == "Atomic `` (KEY `` x)"
-
   "{|x, y, z|}"   == "{|x, {|y, z|}|}"
   "{|x, y|}"      == "MPair x y"