| changeset 5421 | 01fc8d6a40f2 |
| parent 5359 | bd539b72d484 |
| child 5434 | 9b4bed3f394c |
--- a/src/HOL/Auth/OtwayRees.ML Tue Sep 01 15:07:11 1998 +0200 +++ b/src/HOL/Auth/OtwayRees.ML Wed Sep 02 10:35:11 1998 +0200 @@ -31,7 +31,7 @@ (**** Inductive proofs about otway ****) (*Nobody sends themselves messages*) -Goal "evs : otway ==> ALL A X. Says A A X ~: set evs"; +Goal "evs : otway ==> ALL X. Says A A X ~: set evs"; by (etac otway.induct 1); by Auto_tac; qed_spec_mp "not_Says_to_self";