src/HOL/Auth/Public.ML
changeset 4477 b3e5857d8d99
parent 4422 21238c9d363e
child 4686 74a12e86b20b
     1.1 --- a/src/HOL/Auth/Public.ML	Tue Dec 23 11:56:09 1997 +0100
     1.2 +++ b/src/HOL/Auth/Public.ML	Wed Dec 24 10:02:30 1997 +0100
     1.3 @@ -38,16 +38,16 @@
     1.4  (** "Image" equations that hold for injective functions **)
     1.5  
     1.6  goal thy "(invKey x : invKey``A) = (x:A)";
     1.7 -by (Auto_tac());
     1.8 +by Auto_tac;
     1.9  qed "invKey_image_eq";
    1.10  
    1.11  (*holds because invKey is injective*)
    1.12  goal thy "(pubK x : pubK``A) = (x:A)";
    1.13 -by (Auto_tac());
    1.14 +by Auto_tac;
    1.15  qed "pubK_image_eq";
    1.16  
    1.17  goal thy "(priK x ~: pubK``A)";
    1.18 -by (Auto_tac());
    1.19 +by Auto_tac;
    1.20  qed "priK_pubK_image_eq";
    1.21  Addsimps [invKey_image_eq, pubK_image_eq, priK_pubK_image_eq];
    1.22  
    1.23 @@ -67,7 +67,7 @@
    1.24  (*Agents see their own private keys!*)
    1.25  goal thy "Key (priK A) : initState A";
    1.26  by (induct_tac "A" 1);
    1.27 -by (Auto_tac());
    1.28 +by Auto_tac;
    1.29  qed "priK_in_initState";
    1.30  AddIffs [priK_in_initState];
    1.31  
    1.32 @@ -114,7 +114,7 @@
    1.33  
    1.34  goal thy "Nonce N ~: parts (initState B)";
    1.35  by (induct_tac "B" 1);
    1.36 -by (Auto_tac ());
    1.37 +by Auto_tac;
    1.38  qed "Nonce_notin_initState";
    1.39  AddIffs [Nonce_notin_initState];
    1.40