src/HOL/Auth/Message.thy
changeset 14181 942db403d4bb
parent 14145 2e31b8cc8788
child 14200 d8598e24f8fa
     1.1 --- a/src/HOL/Auth/Message.thy	Wed Sep 03 18:20:57 2003 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Thu Sep 04 11:08:24 2003 +0200
     1.3 @@ -23,14 +23,11 @@
     1.4    invKey        :: "key=>key"  --{*inverse of a symmetric key*}
     1.5  
     1.6  specification (invKey)
     1.7 -  invKey_cases: "(\<forall>K. invKey(invKey K) = K) & (all_symmetric --> invKey = id)"
     1.8 +  invKey [simp]: "invKey (invKey K) = K"
     1.9 +  invKey_symmetric: "all_symmetric --> invKey = id"
    1.10      by (rule exI [of _ id], auto)
    1.11  
    1.12  
    1.13 -lemma invKey [simp]: "invKey (invKey K) = K"
    1.14 -by (simp add: invKey_cases)
    1.15 -
    1.16 -
    1.17  text{*The inverse of a symmetric key is itself; that of a public key
    1.18        is the private key and vice versa*}
    1.19