Simplification of definition of synth
authorpaulson
Mon Sep 23 18:18:18 1996 +0200 (1996-09-23)
changeset 20100a22b9d63a18
parent 2009 9023e474d22a
child 2011 d9af64c26be6
Simplification of definition of synth
src/HOL/Auth/Message.thy
     1.1 --- a/src/HOL/Auth/Message.thy	Mon Sep 23 18:12:45 1996 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Mon Sep 23 18:18:18 1996 +0200
     1.3 @@ -100,6 +100,6 @@
     1.4      Inj     "X: H ==> X: synth H"
     1.5      Agent   "Agent agt : synth H"
     1.6      MPair   "[| X: synth H;  Y: synth H |] ==> {|X,Y|} : synth H"
     1.7 -    Crypt   "[| X: synth H; Key(K): synth H |] ==> Crypt X K : synth H"
     1.8 +    Crypt   "[| X: synth H; Key(K): H |] ==> Crypt X K : synth H"
     1.9  
    1.10  end