# HG changeset patch
# User paulson
# Date 905761087 -7200
# Node ID ff11f8b364ef0515e0f1d727913cd821fcba129f
# Parent  d98a55f581c5c0f29c168e84e4e2e813e54eab9f
commented out duplicate proof

diff -r d98a55f581c5 -r ff11f8b364ef src/HOL/UNITY/NSP_Bad.ML
--- a/src/HOL/UNITY/NSP_Bad.ML	Mon Sep 14 10:17:44 1998 +0200
+++ b/src/HOL/UNITY/NSP_Bad.ML	Mon Sep 14 10:18:07 1998 +0200
@@ -65,15 +65,13 @@
     sends messages containing X! **)
 
 (*Spy never sees another agent's private key! (unless it's bad at start)*)
-Goal "Invariant Nprg {s. (Key (priK A) : parts (spies s)) = (A : bad)}";
-by (rtac InvariantI 1);
-by (Force_tac 1);
-by (constrains_tac 1);
-by Auto_tac;
-qed "Spy_see_priK";
-
-(** HOW TO USE??
-Addsimps [Spy_see_priK];
+(*
+    Goal "Invariant Nprg {s. (Key (priK A) : parts (spies s)) = (A : bad)}";
+    by (rtac InvariantI 1);
+    by (Force_tac 1);
+    by (constrains_tac 1);
+    by Auto_tac;
+    qed "Spy_see_priK";
 *)
 
 Goal "s : reachable Nprg ==> (Key (priK A) : parts (spies s)) = (A : bad)";