src/HOL/Auth/OtwayRees_AN.ML
changeset 5421 01fc8d6a40f2
parent 5278 a903b66822e2
child 5434 9b4bed3f394c
     1.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Tue Sep 01 15:07:11 1998 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Wed Sep 02 10:35:11 1998 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4  (**** Inductive proofs about otway ****)
     1.5  
     1.6  (*Nobody sends themselves messages*)
     1.7 -Goal "evs : otway ==> ALL A X. Says A A X ~: set evs";
     1.8 +Goal "evs : otway ==> ALL X. Says A A X ~: set evs";
     1.9  by (etac otway.induct 1);
    1.10  by Auto_tac;
    1.11  qed_spec_mp "not_Says_to_self";