src/HOL/Auth/TLS.ML
changeset 4423 a129b817b58a
parent 4422 21238c9d363e
child 4449 df30e75f670f
     1.1 --- a/src/HOL/Auth/TLS.ML	Tue Dec 16 15:17:26 1997 +0100
     1.2 +++ b/src/HOL/Auth/TLS.ML	Tue Dec 16 17:58:03 1997 +0100
     1.3 @@ -35,13 +35,13 @@
     1.4  (*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***)
     1.5  
     1.6  goal thy "pubK A ~= sessionK arg";
     1.7 -br notI 1;
     1.8 +by (rtac notI 1);
     1.9  by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
    1.10  by (Full_simp_tac 1);
    1.11  qed "pubK_neq_sessionK";
    1.12  
    1.13  goal thy "priK A ~= sessionK arg";
    1.14 -br notI 1;
    1.15 +by (rtac notI 1);
    1.16  by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
    1.17  by (Full_simp_tac 1);
    1.18  qed "priK_neq_sessionK";
    1.19 @@ -274,7 +274,7 @@
    1.20  \             : parts (spies evs);                          \
    1.21  \           evs : tls;  A ~: bad |]                         \
    1.22  \        ==> Notes A {|Agent B, Nonce PMS|} : set evs";
    1.23 -be rev_mp 1;
    1.24 +by (etac rev_mp 1);
    1.25  by (parts_induct_tac 1);
    1.26  by (Fake_parts_insert_tac 1);
    1.27  val lemma = result();