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