Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Auth/Guard/Guard_NS_Public.thy
changeset 21404 eb85850d3eb7
parent 20768 1d478c2d621f
child 23746 a455e69c31cc 
--- 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))"
isabelle