src/HOL/Auth/Shared.thy
changeset 2264 f298678bd54a
parent 2078 b198b3d46fb4
child 2319 95f0d5243c85
     1.1 --- a/src/HOL/Auth/Shared.thy	Wed Nov 27 20:36:33 1996 +0100
     1.2 +++ b/src/HOL/Auth/Shared.thy	Thu Nov 28 10:41:14 1996 +0100
     1.3 @@ -54,9 +54,9 @@
     1.4  rules
     1.5    inj_shrK      "inj shrK"
     1.6  
     1.7 -  inj_newN      "inj newN"
     1.8 +  newN_length   "(newN evs = newN evt) ==> (length evs = length evt)"
     1.9 +  newK_length   "(newK evs = newK evt) ==> (length evs = length evt)"
    1.10  
    1.11 -  inj_newK      "inj newK"
    1.12    newK_neq_shrK "newK evs ~= shrK A" 
    1.13    isSym_newK    "isSymKey (newK evs)"
    1.14