# HG changeset patch
# User paulson
# Date 921750060 -3600
# Node ID 4a9040b85e2ec40cfb27d1cf9a279607e2f610c3
# Parent  e6f0c192ef88b5783f4b13159fab9db641eb9eca
exchanged the order of Gets and Notes in datatype event

diff -r e6f0c192ef88 -r 4a9040b85e2e src/HOL/Auth/Event.ML
--- a/src/HOL/Auth/Event.ML	Wed Mar 17 18:01:41 1999 +0100
+++ b/src/HOL/Auth/Event.ML	Thu Mar 18 10:41:00 1999 +0100
@@ -18,10 +18,10 @@
 	  read_instantiate_sg (sign_of thy) [("H", "knows Spy evs")]);
 
 
-Goal "P(event_case sf nf gf ev) = \
+Goal "P(event_case sf gf nf ev) = \
 \      ((ALL A B X. ev = Says A B X --> P(sf A B X)) & \
-\       (ALL A X. ev = Notes A X --> P(nf A X)) & \
-\       (ALL A X. ev = Gets A X --> P(gf A X)))";
+\       (ALL A X. ev = Gets A X --> P(gf A X)) & \
+\       (ALL A X. ev = Notes A X --> P(nf A X)))";
 by (induct_tac "ev" 1);
 by Auto_tac;
 qed "expand_event_case";
diff -r e6f0c192ef88 -r 4a9040b85e2e src/HOL/Auth/Event.thy
--- a/src/HOL/Auth/Event.thy	Wed Mar 17 18:01:41 1999 +0100
+++ b/src/HOL/Auth/Event.thy	Thu Mar 18 10:41:00 1999 +0100
@@ -16,10 +16,10 @@
 consts  (*Initial states of agents -- parameter of the construction*)
   initState :: agent => msg set
 
-datatype  (*Messages--could add another constructor for agent knowledge*)
+datatype
   event = Says  agent agent msg
+        | Gets  agent       msg
         | Notes agent       msg
-        | Gets  agent       msg
        
 consts 
   bad    :: agent set        (*compromised agents*)
@@ -41,21 +41,22 @@
 
 primrec
   knows_Nil   "knows A []         = initState A"
-  knows_Cons  "knows A (ev # evs) =
-	        (if A = Spy then 
-                  (case ev of
-		    Says A' B X => insert X (knows Spy evs)
-		  | Notes A' X  => 
-                   if A' : bad then insert X (knows Spy evs) else knows Spy evs
-                  | Gets A' X => knows Spy evs)
-                 else
-                  (case ev of
-		    Says A' B X => 
-                      if A'=A then insert X (knows A evs) else knows A evs
-		  | Notes A' X    => 
-                      if A'=A then insert X (knows A evs) else knows A evs
-		  | Gets A' X    => 
-                      if A'=A then insert X (knows A evs) else knows A evs))"
+  knows_Cons
+    "knows A (ev # evs) =
+       (if A = Spy then 
+	(case ev of
+	   Says A' B X => insert X (knows Spy evs)
+	 | Gets A' X => knows Spy evs
+	 | Notes A' X  => 
+	     if A' : bad then insert X (knows Spy evs) else knows Spy evs)
+	else
+	(case ev of
+	   Says A' B X => 
+	     if A'=A then insert X (knows A evs) else knows A evs
+	 | Gets A' X    => 
+	     if A'=A then insert X (knows A evs) else knows A evs
+	 | Notes A' X    => 
+	     if A'=A then insert X (knows A evs) else knows A evs))"
 
 (*
   Case A=Spy on the Gets event
@@ -73,8 +74,8 @@
   used_Cons  "used (ev # evs) =
 	         (case ev of
 		    Says A B X => parts {X} Un (used evs)
-		  | Notes A X  => parts {X} Un (used evs)
-		  | Gets A X   => used evs)"
+		  | Gets A X   => used evs
+		  | Notes A X  => parts {X} Un (used evs))"