src/HOL/Auth/Event.thy
changeset 5183 89f162de39cf
parent 3683 aafe719dff14
child 6308 76f3865a2b1d
     1.1 --- a/src/HOL/Auth/Event.thy	Fri Jul 24 13:02:01 1998 +0200
     1.2 +++ b/src/HOL/Auth/Event.thy	Fri Jul 24 13:03:20 1998 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4    Spy_in_bad     "Spy: bad"
     1.5    Server_not_bad "Server ~: bad"
     1.6  
     1.7 -primrec spies list
     1.8 +primrec
     1.9             (*Spy reads all traffic whether addressed to him or not*)
    1.10    spies_Nil   "spies []       = initState Spy"
    1.11    spies_Cons  "spies (ev # evs) =
    1.12 @@ -43,7 +43,7 @@
    1.13      complement of the set of fresh items*)
    1.14    used :: event list => msg set
    1.15  
    1.16 -primrec used list
    1.17 +primrec
    1.18    used_Nil   "used []         = (UN B. parts (initState B))"
    1.19    used_Cons  "used (ev # evs) =
    1.20  	         (case ev of