Tidied using rev_iffD1
authorpaulson
Tue Dec 23 11:56:09 1997 +0100 (1997-12-23)
changeset 4476fbdc87f8ac7e
parent 4475 09864e2536d3
child 4477 b3e5857d8d99
Tidied using rev_iffD1
src/HOL/Auth/NS_Public_Bad.ML
     1.1 --- a/src/HOL/Auth/NS_Public_Bad.ML	Tue Dec 23 11:51:43 1997 +0100
     1.2 +++ b/src/HOL/Auth/NS_Public_Bad.ML	Tue Dec 23 11:56:09 1997 +0100
     1.3 @@ -67,13 +67,8 @@
     1.4  qed "Spy_analz_priK";
     1.5  Addsimps [Spy_analz_priK];
     1.6  
     1.7 -goal thy  "!!A. [| Key (priK A) : parts (spies evs);       \
     1.8 -\                  evs : ns_public |] ==> A:bad";
     1.9 -by (blast_tac (claset() addDs [Spy_see_priK]) 1);
    1.10 -qed "Spy_see_priK_D";
    1.11 -
    1.12 -bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D);
    1.13 -AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
    1.14 +AddSDs [Spy_see_priK RSN (2, rev_iffD1), 
    1.15 +	Spy_analz_priK RSN (2, rev_iffD1)];
    1.16  
    1.17  
    1.18  (**** Authenticity properties obtained from NS2 ****)
    1.19 @@ -104,7 +99,8 @@
    1.20  by (etac rev_mp 1);
    1.21  by (parts_induct_tac 1);
    1.22  by (ALLGOALS
    1.23 -    (asm_simp_tac (simpset() addsimps [all_conj_distrib, parts_insert_spies])));
    1.24 +    (asm_simp_tac (simpset() addsimps [all_conj_distrib, 
    1.25 +				       parts_insert_spies])));
    1.26  (*NS1*)
    1.27  by (expand_case_tac "NA = ?y" 2 THEN blast_tac (claset() addSEs partsEs) 2);
    1.28  (*Fake*)
    1.29 @@ -138,7 +134,7 @@
    1.30  by (analz_induct_tac 1);
    1.31  (*NS3*)
    1.32  by (blast_tac (claset() addDs  [Says_imp_spies RS parts.Inj]
    1.33 -                       addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
    1.34 +                        addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
    1.35  (*NS2*)
    1.36  by (blast_tac (claset() addSEs [MPair_parts]
    1.37  		       addDs  [Says_imp_spies RS parts.Inj,