src/HOL/Auth/Message.thy
changeset 5652 fe5f5510aef4
parent 5234 701fa0ed77b7
child 6807 6737af18317e
equal deleted inserted replaced
5651:ca45d6126c8a 5652:fe5f5510aef4
     5 
     5 
     6 Datatypes of agents and messages;
     6 Datatypes of agents and messages;
     7 Inductive relations "parts", "analz" and "synth"
     7 Inductive relations "parts", "analz" and "synth"
     8 *)
     8 *)
     9 
     9 
    10 Message = Datatype +
    10 Message = Main +
    11 
       
    12 (*Is there a difference between a nonce and arbitrary numerical data?
       
    13   Do we need a type of nonces?*)
       
    14 
    11 
    15 types 
    12 types 
    16   key = nat
    13   key = nat
    17 
    14 
    18 consts
    15 consts