1.1 --- a/src/HOL/Auth/ZhouGollmann.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Auth/ZhouGollmann.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -21,8 +21,7 @@
     1.4  abbreviation f_con :: nat where "f_con == 4"
     1.5  
     1.6  
     1.7 -constdefs
     1.8 -  broken :: "agent set"    
     1.9 +definition broken :: "agent set" where    
    1.10      --{*the compromised honest agents; TTP is included as it's not allowed to
    1.11          use the protocol*}
    1.12     "broken == bad - {Spy}"