# HG changeset patch
# User krauss
# Date 1250278574 -7200
# Node ID 99dc5b7b468704e5312f54510babb01a6b7c5abd
# Parent  66b4946d9483fa9fc2d6f19463b8e766a9acf22a
removed atp_minimize invocation

diff -r 66b4946d9483 -r 99dc5b7b4687 src/HOL/Auth/Yahalom.thy
--- a/src/HOL/Auth/Yahalom.thy	Fri Aug 14 21:28:58 2009 +0200
+++ b/src/HOL/Auth/Yahalom.thy	Fri Aug 14 21:36:14 2009 +0200
@@ -633,6 +633,5 @@
          (\<forall>NA k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs);
          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
       ==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
-atp_minimize [atp=spass] A_Said_YM3_lemma B_gets_good_key Gets_imp_analz_Spy YM4_parts_knows_Spy analz.Fst not_parts_not_analz
 by (metis A_Said_YM3_lemma B_gets_good_key Gets_imp_analz_Spy YM4_parts_knows_Spy analz.Fst not_parts_not_analz)
 end