src/HOL/Auth/Yahalom.thy
changeset 2378 fc103154ad8f
parent 2284 80ebd1a213fd
child 2451 ce85a2aafc7a
equal deleted inserted replaced
2377:ad9d2dedaeaa 2378:fc103154ad8f
    10   Proc. Royal Soc. 426 (1989)
    10   Proc. Royal Soc. 426 (1989)
    11 *)
    11 *)
    12 
    12 
    13 Yahalom = Shared + 
    13 Yahalom = Shared + 
    14 
    14 
    15 consts  yahalom   :: "agent set => event list set"
    15 consts  yahalom   :: agent set => event list set
    16 inductive "yahalom lost"
    16 inductive "yahalom lost"
    17   intrs 
    17   intrs 
    18          (*Initial trace is empty*)
    18          (*Initial trace is empty*)
    19     Nil  "[]: yahalom lost"
    19     Nil  "[]: yahalom lost"
    20 
    20