# HG changeset patch
# User paulson
# Date 982149769 -3600
# Node ID ac51bafd1afbdc171f88928c55148804fcd2d608
# Parent  285b31e9e02602f3daf43e04eb7d93163046bb56
not_bad_tac is obsolete

diff -r 285b31e9e026 -r ac51bafd1afb src/HOL/Auth/Public_lemmas.ML
--- a/src/HOL/Auth/Public_lemmas.ML	Wed Feb 14 12:16:32 2001 +0100
+++ b/src/HOL/Auth/Public_lemmas.ML	Wed Feb 14 12:22:49 2001 +0100
@@ -91,25 +91,6 @@
 AddSIs  [Spy_spies_bad];
 
 
-(*For not_bad_tac*)
-Goal "[| Crypt (pubK A) X : analz (spies evs);  A: bad |] \
-\           ==> X : analz (spies evs)";
-by (blast_tac (claset() addSDs [analz.Decrypt]) 1);
-qed "Crypt_Spy_analz_bad";
-
-(*Prove that the agent is uncompromised by the confidentiality of 
-  a component of a message she's said.*)
-fun not_bad_tac s =
-    case_tac ("(" ^ s ^ ") : bad") THEN'
-    SELECT_GOAL 
-      (REPEAT_DETERM (dtac (Says_imp_spies RS analz.Inj) 1) THEN
-       REPEAT_DETERM (etac MPair_analz 1) THEN
-       THEN_BEST_FIRST 
-         (dres_inst_tac [("A", s)] Crypt_Spy_analz_bad 1 THEN assume_tac 1)
-         (has_fewer_prems 1, size_of_thm)
-         Safe_tac);
-
-
 (*** Fresh nonces ***)
 
 Goal "Nonce N ~: parts (initState B)";