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