# HG changeset patch
# User bulwahn
# Date 1283272710 -7200
# Node ID b1a7bef0907a1042875e119ae3a7219f604234b1
# Parent  b5d126d7be4b07c4b6f021f1582613f39240eed3
renewing specifications in HOL-Auth

diff -r b5d126d7be4b -r b1a7bef0907a src/HOL/Auth/Event.thy
--- a/src/HOL/Auth/Event.thy	Tue Aug 31 15:21:56 2010 +0200
+++ b/src/HOL/Auth/Event.thy	Tue Aug 31 18:38:30 2010 +0200
@@ -22,14 +22,6 @@
        
 consts 
   bad    :: "agent set"                         -- {* compromised agents *}
-  knows  :: "agent => event list => msg set"
-
-
-text{*The constant "spies" is retained for compatibility's sake*}
-
-abbreviation (input)
-  spies  :: "event list => msg set" where
-  "spies == knows Spy"
 
 text{*Spy has access to his own key for spoof messages, but Server is secure*}
 specification (bad)
@@ -37,9 +29,10 @@
   Server_not_bad [iff]: "Server \<notin> bad"
     by (rule exI [of _ "{Spy}"], simp)
 
-primrec
+primrec knows :: "agent => event list => msg set"
+where
   knows_Nil:   "knows A [] = initState A"
-  knows_Cons:
+| knows_Cons:
     "knows A (ev # evs) =
        (if A = Spy then 
         (case ev of
@@ -62,14 +55,20 @@
   therefore the oops case must use Notes
 *)
 
-consts
-  (*Set of items that might be visible to somebody:
+text{*The constant "spies" is retained for compatibility's sake*}
+
+abbreviation (input)
+  spies  :: "event list => msg set" where
+  "spies == knows Spy"
+
+
+(*Set of items that might be visible to somebody:
     complement of the set of fresh items*)
-  used :: "event list => msg set"
 
-primrec
+primrec used :: "event list => msg set"
+where
   used_Nil:   "used []         = (UN B. parts (initState B))"
-  used_Cons:  "used (ev # evs) =
+| used_Cons:  "used (ev # evs) =
                      (case ev of
                         Says A B X => parts {X} \<union> used evs
                       | Gets A X   => used evs
diff -r b5d126d7be4b -r b1a7bef0907a src/HOL/Auth/NS_Public_Bad.thy
--- a/src/HOL/Auth/NS_Public_Bad.thy	Tue Aug 31 15:21:56 2010 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.thy	Tue Aug 31 18:38:30 2010 +0200
@@ -203,7 +203,7 @@
 apply clarify
 apply (frule_tac A' = A in 
        Says_imp_knows_Spy [THEN parts.Inj, THEN unique_NB], auto)
-apply (rename_tac C B' evs3)
+apply (rename_tac evs3 B' C)
 txt{*This is the attack!
 @{subgoals[display,indent=0,margin=65]}
 *}