src/HOL/Auth/Guard/OtwayRees.thy
changeset 16417 9bc16273c2d4
parent 13508 890d736b93a5
equal deleted inserted replaced
16416:6061ae1f90f2 16417:9bc16273c2d4
     9 Cambridge CB3 0FD, United Kingdom
     9 Cambridge CB3 0FD, United Kingdom
    10 ******************************************************************************)
    10 ******************************************************************************)
    11 
    11 
    12 header{*Otway-Rees Protocol*}
    12 header{*Otway-Rees Protocol*}
    13 
    13 
    14 theory OtwayRees = Guard_Shared:
    14 theory OtwayRees imports Guard_Shared begin
    15 
    15 
    16 subsection{*messages used in the protocol*}
    16 subsection{*messages used in the protocol*}
    17 
    17 
    18 syntax nil :: "msg"
    18 syntax nil :: "msg"
    19 
    19