# HG changeset patch
# User paulson
# Date 853752058 -3600
# Node ID e40ca839758d94c690382e5f0edd64e4e119eba3
# Parent  bc6e29c776d6e3044960d7a0bd3a0e91d0a74843
Simplified Oops case of main theorem

diff -r bc6e29c776d6 -r e40ca839758d src/HOL/Auth/NS_Shared.ML
--- a/src/HOL/Auth/NS_Shared.ML	Mon Jan 20 10:18:47 1997 +0100
+++ b/src/HOL/Auth/NS_Shared.ML	Mon Jan 20 10:20:58 1997 +0100
@@ -298,17 +298,10 @@
 by (fast_tac (!claset addSEs sees_Spy_partsEs
                       addIs [parts_insertI, impOfSubs analz_subset_parts]
                       addss (!simpset)) 1);
-(*NS3 and Oops subcases*) (**LEVEL 5 **)
+(*Oops*)
+by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 2);
+(*NS3*) (**LEVEL 6 **)
 by (step_tac (!claset delrules [impCE]) 1);
-by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
-by (etac conjE 2);
-by (mp_tac 2);
-(**LEVEL 9 **)
-by (forward_tac [Says_imp_sees_Spy RS parts.Inj RS A_trusts_NS2] 2);
-by (assume_tac 3);
-by (fast_tac (!claset addSEs [Says_Crypt_not_lost]) 2);
-by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 2);
-(*NS3*)
 by (forward_tac [Says_imp_sees_Spy RS parts.Inj RS A_trusts_NS2] 1);
 by (assume_tac 2);
 by (fast_tac (!claset addSEs [Says_Crypt_not_lost]) 1);