diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Auth/Guard/Guard_NS_Public.thy
--- a/src/HOL/Auth/Guard/Guard_NS_Public.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Auth/Guard/Guard_NS_Public.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -18,19 +18,23 @@
 subsection{*messages used in the protocol*}
 
 abbreviation (input)
-  ns1 :: "agent => agent => nat => event"
+  ns1 :: "agent => agent => nat => event" where
   "ns1 A B NA == Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})"
 
-  ns1' :: "agent => agent => agent => nat => event"
+abbreviation (input)
+  ns1' :: "agent => agent => agent => nat => event" where
   "ns1' A' A B NA == Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})"
 
-  ns2 :: "agent => agent => nat => nat => event"
+abbreviation (input)
+  ns2 :: "agent => agent => nat => nat => event" where
   "ns2 B A NA NB == Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
 
-  ns2' :: "agent => agent => agent => nat => nat => event"
+abbreviation (input)
+  ns2' :: "agent => agent => agent => nat => nat => event" where
   "ns2' B' B A NA NB == Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
 
-  ns3 :: "agent => agent => nat => event"
+abbreviation (input)
+  ns3 :: "agent => agent => nat => event" where
   "ns3 A B NB == Says A B (Crypt (pubK B) (Nonce NB))"