src/HOL/Auth/OtwayRees_AN.thy
changeset 2378 fc103154ad8f
parent 2284 80ebd1a213fd
child 2451 ce85a2aafc7a
equal deleted inserted replaced
2377:ad9d2dedaeaa 2378:fc103154ad8f
    12   IEEE Trans. SE 22 (1), 1996
    12   IEEE Trans. SE 22 (1), 1996
    13 *)
    13 *)
    14 
    14 
    15 OtwayRees_AN = Shared + 
    15 OtwayRees_AN = Shared + 
    16 
    16 
    17 consts  otway   :: "agent set => event list set"
    17 consts  otway   :: agent set => event list set
    18 inductive "otway lost"
    18 inductive "otway lost"
    19   intrs 
    19   intrs 
    20          (*Initial trace is empty*)
    20          (*Initial trace is empty*)
    21     Nil  "[]: otway lost"
    21     Nil  "[]: otway lost"
    22 
    22