1.1 --- a/src/HOL/Auth/ZhouGollmann.thy	Thu Sep 28 23:42:32 2006 +0200
     1.2 +++ b/src/HOL/Auth/ZhouGollmann.thy	Thu Sep 28 23:42:35 2006 +0200
     1.3 @@ -12,23 +12,18 @@
     1.4  
     1.5  theory ZhouGollmann imports Public begin
     1.6  
     1.7 -syntax
     1.8 +abbreviation
     1.9    TTP :: agent
    1.10 +  "TTP == Server"
    1.11  
    1.12 -translations
    1.13 -  "TTP" == " Server "
    1.14 -
    1.15 -syntax
    1.16    f_sub :: nat
    1.17 +  "f_sub == 5"
    1.18    f_nro :: nat
    1.19 +  "f_nro == 2"
    1.20    f_nrr :: nat
    1.21 +  "f_nrr == 3"
    1.22    f_con :: nat
    1.23 -
    1.24 -translations
    1.25 -  "f_sub" == " 5 "
    1.26 -  "f_nro" == " 2 "
    1.27 -  "f_nrr" == " 3 "
    1.28 -  "f_con" == " 4 "
    1.29 +  "f_con == 4"
    1.30  
    1.31  
    1.32  constdefs