src/HOL/SET_Protocol/Event_SET.thy

--- a/src/HOL/SET_Protocol/Event_SET.thy	Wed Feb 10 19:37:34 2010 +0100
+++ b/src/HOL/SET_Protocol/Event_SET.thy	Wed Feb 10 23:53:46 2010 +0100
@@ -11,8 +11,7 @@
 begin
 
 text{*The Root Certification Authority*}
-syntax        RCA :: agent
-translations "RCA" == "CA 0"
+abbreviation "RCA == CA 0"
 
 
 text{*Message events*}