src/HOL/Auth/NS_Shared.ML
changeset 4477 b3e5857d8d99
parent 4470 af3239def3d4
child 4509 828148415197
     1.1 --- a/src/HOL/Auth/NS_Shared.ML	Tue Dec 23 11:56:09 1997 +0100
     1.2 +++ b/src/HOL/Auth/NS_Shared.ML	Wed Dec 24 10:02:30 1997 +0100
     1.3 @@ -45,7 +45,7 @@
     1.4  (*Nobody sends themselves messages*)
     1.5  goal thy "!!evs. evs : ns_shared ==> ALL A X. Says A A X ~: set evs";
     1.6  by (etac ns_shared.induct 1);
     1.7 -by (Auto_tac());
     1.8 +by Auto_tac;
     1.9  qed_spec_mp "not_Says_to_self";
    1.10  Addsimps [not_Says_to_self];
    1.11  AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    1.12 @@ -84,7 +84,7 @@
    1.13  
    1.14  goal thy 
    1.15   "!!evs. evs : ns_shared ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
    1.16 -by (Auto_tac());
    1.17 +by Auto_tac;
    1.18  qed "Spy_analz_shrK";
    1.19  Addsimps [Spy_analz_shrK];
    1.20  
    1.21 @@ -124,7 +124,7 @@
    1.22  \            K' = shrK A";
    1.23  by (etac rev_mp 1);
    1.24  by (etac ns_shared.induct 1);
    1.25 -by (Auto_tac());
    1.26 +by Auto_tac;
    1.27  qed "Says_Server_message_form";
    1.28  
    1.29  
    1.30 @@ -193,7 +193,7 @@
    1.31  by (blast_tac (claset() addSEs partsEs
    1.32                          addDs [impOfSubs parts_insert_subset_Un]) 1);
    1.33  (*Base, NS4 and NS5*)
    1.34 -by (Auto_tac());
    1.35 +by Auto_tac;
    1.36  result();
    1.37  
    1.38