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