src/HOL/Auth/CertifiedEmail.thy

--- a/src/HOL/Auth/CertifiedEmail.thy	Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/CertifiedEmail.thy	Thu Sep 28 23:42:35 2006 +0200
@@ -7,13 +7,12 @@
 
 theory CertifiedEmail imports Public begin
 
-syntax
-  TTP        :: agent
-  RPwd       :: "agent => key"
+abbreviation
+  TTP :: agent
+  "TTP == Server"
 
-translations
-  "TTP"   == "Server "
-  "RPwd"  == "shrK "
+  RPwd :: "agent => key"
+  "RPwd == shrK"
 
  
 (*FIXME: the four options should be represented by pairs of 0 or 1.