src/HOL/Auth/ZhouGollmann.thy
changeset 21404 eb85850d3eb7
parent 20768 1d478c2d621f
child 23746 a455e69c31cc
     1.1 --- a/src/HOL/Auth/ZhouGollmann.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/Auth/ZhouGollmann.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -13,17 +13,12 @@
     1.4  theory ZhouGollmann imports Public begin
     1.5  
     1.6  abbreviation
     1.7 -  TTP :: agent
     1.8 -  "TTP == Server"
     1.9 +  TTP :: agent where "TTP == Server"
    1.10  
    1.11 -  f_sub :: nat
    1.12 -  "f_sub == 5"
    1.13 -  f_nro :: nat
    1.14 -  "f_nro == 2"
    1.15 -  f_nrr :: nat
    1.16 -  "f_nrr == 3"
    1.17 -  f_con :: nat
    1.18 -  "f_con == 4"
    1.19 +abbreviation f_sub :: nat where "f_sub == 5"
    1.20 +abbreviation f_nro :: nat where "f_nro == 2"
    1.21 +abbreviation f_nrr :: nat where "f_nrr == 3"
    1.22 +abbreviation f_con :: nat where "f_con == 4"
    1.23  
    1.24  
    1.25  constdefs