src/HOL/Auth/Shared.ML
changeset 4477 b3e5857d8d99
parent 4423 a129b817b58a
child 4509 828148415197
     1.1 --- a/src/HOL/Auth/Shared.ML	Tue Dec 23 11:56:09 1997 +0100
     1.2 +++ b/src/HOL/Auth/Shared.ML	Wed Dec 24 10:02:30 1997 +0100
     1.3 @@ -24,7 +24,7 @@
     1.4  
     1.5  goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
     1.6  by (induct_tac "C" 1);
     1.7 -by (Auto_tac ());
     1.8 +by Auto_tac;
     1.9  qed "keysFor_parts_initState";
    1.10  Addsimps [keysFor_parts_initState];
    1.11  
    1.12 @@ -70,7 +70,7 @@
    1.13  (*Agents see their own shared keys!*)
    1.14  goal thy "Key (shrK A) : initState A";
    1.15  by (induct_tac "A" 1);
    1.16 -by (Auto_tac());
    1.17 +by Auto_tac;
    1.18  qed "shrK_in_initState";
    1.19  AddIffs [shrK_in_initState];
    1.20  
    1.21 @@ -97,7 +97,7 @@
    1.22  
    1.23  goal thy "Nonce N ~: parts (initState B)";
    1.24  by (induct_tac "B" 1);
    1.25 -by (Auto_tac ());
    1.26 +by Auto_tac;
    1.27  qed "Nonce_notin_initState";
    1.28  AddIffs [Nonce_notin_initState];
    1.29  
    1.30 @@ -169,7 +169,7 @@
    1.31  by (etac exE 1);
    1.32  by (cut_inst_tac [("evs","evs'")] 
    1.33      (Finites.emptyI RS Finites.insertI RS Key_supply_ax) 1);
    1.34 -by (Auto_tac());
    1.35 +by Auto_tac;
    1.36  qed "Key_supply2";
    1.37  
    1.38  goal thy "EX K K' K''. Key K ~: used evs & Key K' ~: used evs' & \