# HG changeset patch # User paulson # Date 843495498 -7200 # Node ID 0a22b9d63a1808b7ba02b2ce6b829a0d9c302b79 # Parent 9023e474d22a8cddf2ccbf730919805d49834142 Simplification of definition of synth diff -r 9023e474d22a -r 0a22b9d63a18 src/HOL/Auth/Message.thy --- 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