src/HOL/Auth/Message.ML
changeset 4477 b3e5857d8d99
parent 4422 21238c9d363e
child 4556 e7a4683c0026
     1.1 --- a/src/HOL/Auth/Message.ML	Tue Dec 23 11:56:09 1997 +0100
     1.2 +++ b/src/HOL/Auth/Message.ML	Wed Dec 24 10:02:30 1997 +0100
     1.3 @@ -20,15 +20,15 @@
     1.4  
     1.5  (*Equations hold because constructors are injective; cannot prove for all f*)
     1.6  goal thy "(Friend x : Friend``A) = (x:A)";
     1.7 -by (Auto_tac());
     1.8 +by Auto_tac;
     1.9  qed "Friend_image_eq";
    1.10  
    1.11  goal thy "(Key x : Key``A) = (x:A)";
    1.12 -by (Auto_tac());
    1.13 +by Auto_tac;
    1.14  qed "Key_image_eq";
    1.15  
    1.16  goal thy "(Nonce x ~: Key``A)";
    1.17 -by (Auto_tac());
    1.18 +by Auto_tac;
    1.19  qed "Nonce_Key_image_eq";
    1.20  Addsimps [Friend_image_eq, Key_image_eq, Nonce_Key_image_eq];
    1.21  
    1.22 @@ -90,7 +90,7 @@
    1.23  
    1.24  goalw thy [keysFor_def]
    1.25      "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)";
    1.26 -by (Auto_tac());
    1.27 +by Auto_tac;
    1.28  qed "keysFor_insert_Crypt";
    1.29  
    1.30  Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, 
    1.31 @@ -101,7 +101,7 @@
    1.32  	keysFor_UN RS equalityD1 RS subsetD RS UN_E];
    1.33  
    1.34  goalw thy [keysFor_def] "keysFor (Key``E) = {}";
    1.35 -by (Auto_tac ());
    1.36 +by Auto_tac;
    1.37  qed "keysFor_image_Key";
    1.38  Addsimps [keysFor_image_Key];
    1.39  
    1.40 @@ -235,7 +235,7 @@
    1.41  goal thy "!!H. [| Y: parts (insert X G);  X: parts H |] \
    1.42  \              ==> Y: parts (G Un H)";
    1.43  by (etac parts_trans 1);
    1.44 -by (Auto_tac());
    1.45 +by Auto_tac;
    1.46  qed "parts_cut";
    1.47  
    1.48  goal thy "!!H. X: parts H ==> parts (insert X H) = parts H";
    1.49 @@ -279,7 +279,7 @@
    1.50  by (rtac equalityI 1);
    1.51  by (rtac subsetI 1);
    1.52  by (etac parts.induct 1);
    1.53 -by (Auto_tac());
    1.54 +by Auto_tac;
    1.55  by (etac parts.induct 1);
    1.56  by (ALLGOALS (blast_tac (claset() addIs [parts.Body])));
    1.57  qed "parts_insert_Crypt";
    1.58 @@ -289,7 +289,7 @@
    1.59  by (rtac equalityI 1);
    1.60  by (rtac subsetI 1);
    1.61  by (etac parts.induct 1);
    1.62 -by (Auto_tac());
    1.63 +by Auto_tac;
    1.64  by (etac parts.induct 1);
    1.65  by (ALLGOALS (blast_tac (claset() addIs [parts.Fst, parts.Snd])));
    1.66  qed "parts_insert_MPair";
    1.67 @@ -300,9 +300,9 @@
    1.68  
    1.69  
    1.70  goal thy "parts (Key``N) = Key``N";
    1.71 -by (Auto_tac());
    1.72 +by Auto_tac;
    1.73  by (etac parts.induct 1);
    1.74 -by (Auto_tac());
    1.75 +by Auto_tac;
    1.76  qed "parts_image_Key";
    1.77  Addsimps [parts_image_Key];
    1.78  
    1.79 @@ -359,9 +359,9 @@
    1.80  Addsimps [parts_analz];
    1.81  
    1.82  goal thy "analz (parts H) = parts H";
    1.83 -by (Auto_tac());
    1.84 +by Auto_tac;
    1.85  by (etac analz.induct 1);
    1.86 -by (Auto_tac());
    1.87 +by Auto_tac;
    1.88  qed "analz_parts";
    1.89  Addsimps [analz_parts];
    1.90  
    1.91 @@ -427,7 +427,7 @@
    1.92  by (rtac equalityI 1);
    1.93  by (rtac subsetI 1);
    1.94  by (etac analz.induct 1);
    1.95 -by (Auto_tac());
    1.96 +by Auto_tac;
    1.97  by (etac analz.induct 1);
    1.98  by (ALLGOALS (blast_tac (claset() addIs [analz.Fst, analz.Snd])));
    1.99  qed "analz_insert_MPair";
   1.100 @@ -450,9 +450,9 @@
   1.101  goal thy "!!H. Key (invKey K) : analz H ==>  \
   1.102  \              insert (Crypt K X) (analz (insert X H)) <= \
   1.103  \              analz (insert (Crypt K X) H)";
   1.104 -by (Auto_tac());
   1.105 +by Auto_tac;
   1.106  by (eres_inst_tac [("za","x")] analz.induct 1);
   1.107 -by (Auto_tac());
   1.108 +by Auto_tac;
   1.109  by (blast_tac (claset() addIs [analz_insertI, analz.Decrypt]) 1);
   1.110  val lemma2 = result();
   1.111  
   1.112 @@ -484,14 +484,14 @@
   1.113  \          insert (Crypt K X) (analz (insert X H))";
   1.114  by (rtac subsetI 1);
   1.115  by (etac analz.induct 1);
   1.116 -by (Auto_tac());
   1.117 +by Auto_tac;
   1.118  qed "analz_insert_Crypt_subset";
   1.119  
   1.120  
   1.121  goal thy "analz (Key``N) = Key``N";
   1.122 -by (Auto_tac());
   1.123 +by Auto_tac;
   1.124  by (etac analz.induct 1);
   1.125 -by (Auto_tac());
   1.126 +by Auto_tac;
   1.127  qed "analz_image_Key";
   1.128  
   1.129  Addsimps [analz_image_Key];
   1.130 @@ -808,7 +808,7 @@
   1.131  qed "MPair_eq_HPair";
   1.132  
   1.133  goalw thy [HPair_def] "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)";
   1.134 -by (Auto_tac());
   1.135 +by Auto_tac;
   1.136  qed "HPair_eq_MPair";
   1.137  
   1.138  AddIffs [HPair_eq, MPair_eq_HPair, HPair_eq_MPair];