src/HOL/Auth/Shared.thy
changeset 3414 804c8a178a7f
parent 2516 4d68fbe6378b
child 3472 fb3c38c88c08
     1.1 --- a/src/HOL/Auth/Shared.thy	Thu Jun 05 14:39:22 1997 +0200
     1.2 +++ b/src/HOL/Auth/Shared.thy	Thu Jun 05 14:40:35 1997 +0200
     1.3 @@ -59,7 +59,7 @@
     1.4      assumes that their keys are dispersed so as to leave room for infinitely
     1.5      many fresh session keys.  We could, alternatively, restrict agents to
     1.6      an unspecified finite number.*)
     1.7 -  Key_supply_ax  "KK: Fin UNIV ==> EX K. K ~: KK & Key K ~: used evs"
     1.8 +  Key_supply_ax  "finite KK ==> EX K. K ~: KK & Key K ~: used evs"
     1.9  
    1.10  
    1.11  (*Agents generate random (symmetric) keys and nonces.