changeset 2010 | 0a22b9d63a18 |
parent 1947 | f19a801a2bca |
child 2032 | 1bbf1bdcaf56 |
--- a/src/HOL/Auth/Message.thy Mon Sep 23 18:12:45 1996 +0200 +++ b/src/HOL/Auth/Message.thy Mon Sep 23 18:18:18 1996 +0200 @@ -100,6 +100,6 @@ Inj "X: H ==> X: synth H" Agent "Agent agt : synth H" MPair "[| X: synth H; Y: synth H |] ==> {|X,Y|} : synth H" - Crypt "[| X: synth H; Key(K): synth H |] ==> Crypt X K : synth H" + Crypt "[| X: synth H; Key(K): H |] ==> Crypt X K : synth H" end