src/HOL/Auth/Public.thy

--- a/src/HOL/Auth/Public.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Auth/Public.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -21,19 +21,24 @@
   publicKey :: "[keymode,agent] => key"
 
 abbreviation
-  pubEK :: "agent => key"
+  pubEK :: "agent => key" where
   "pubEK == publicKey Encryption"
 
-  pubSK :: "agent => key"
+abbreviation
+  pubSK :: "agent => key" where
   "pubSK == publicKey Signature"
 
-  privateKey :: "[keymode, agent] => key"
+abbreviation
+  privateKey :: "[keymode, agent] => key" where
   "privateKey b A == invKey (publicKey b A)"
 
+abbreviation
   (*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*)
-  priEK :: "agent => key"
+  priEK :: "agent => key" where
   "priEK A == privateKey Encryption A"
-  priSK :: "agent => key"
+
+abbreviation
+  priSK :: "agent => key" where
   "priSK A == privateKey Signature A"
 
 
@@ -41,10 +46,11 @@
 simple situation where the signature and encryption keys are the same.*}
 
 abbreviation
-  pubK :: "agent => key"
+  pubK :: "agent => key" where
   "pubK A == pubEK A"
 
-  priK :: "agent => key"
+abbreviation
+  priK :: "agent => key" where
   "priK A == invKey (pubEK A)"