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