author | paulson |
Mon, 23 Sep 1996 18:18:18 +0200 | |
changeset 2010 | 0a22b9d63a18 |
parent 2009 | 9023e474d22a |
child 2011 | d9af64c26be6 |
--- 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