# HG changeset patch
# User paulson
# Date 1062666504 -7200
# Node ID 942db403d4bbec31a956581097db57cb9eb98d0e
# Parent  d2e550609c408d8056e498b822ea781f749f5239
new, separate specifications

diff -r d2e550609c40 -r 942db403d4bb src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Wed Sep 03 18:20:57 2003 +0200
+++ b/src/HOL/Auth/Message.thy	Thu Sep 04 11:08:24 2003 +0200
@@ -23,14 +23,11 @@
   invKey        :: "key=>key"  --{*inverse of a symmetric key*}
 
 specification (invKey)
-  invKey_cases: "(\<forall>K. invKey(invKey K) = K) & (all_symmetric --> invKey = id)"
+  invKey [simp]: "invKey (invKey K) = K"
+  invKey_symmetric: "all_symmetric --> invKey = id"
     by (rule exI [of _ id], auto)
 
 
-lemma invKey [simp]: "invKey (invKey K) = K"
-by (simp add: invKey_cases)
-
-
 text{*The inverse of a symmetric key is itself; that of a public key
       is the private key and vice versa*}
 
diff -r d2e550609c40 -r 942db403d4bb src/HOL/Auth/Shared.thy
--- a/src/HOL/Auth/Shared.thy	Wed Sep 03 18:20:57 2003 +0200
+++ b/src/HOL/Auth/Shared.thy	Thu Sep 04 11:08:24 2003 +0200
@@ -25,7 +25,7 @@
 defs  all_symmetric_def: "all_symmetric == True"
 
 lemma isSym_keys: "K \<in> symKeys"	
-by (simp add: symKeys_def all_symmetric_def invKey_cases) 
+by (simp add: symKeys_def all_symmetric_def invKey_symmetric) 
 
 text{*Server knows all long-term keys; other agents know only their own*}
 primrec