equal
deleted
inserted
replaced
23 |
23 |
24 |
24 |
25 (**** Inductive proofs about ns_public ****) |
25 (**** Inductive proofs about ns_public ****) |
26 |
26 |
27 (*Nobody sends themselves messages*) |
27 (*Nobody sends themselves messages*) |
28 Goal "evs : ns_public ==> ALL A X. Says A A X ~: set evs"; |
28 Goal "evs : ns_public ==> ALL X. Says A A X ~: set evs"; |
29 by (etac ns_public.induct 1); |
29 by (etac ns_public.induct 1); |
30 by Auto_tac; |
30 by Auto_tac; |
31 qed_spec_mp "not_Says_to_self"; |
31 qed_spec_mp "not_Says_to_self"; |
32 Addsimps [not_Says_to_self]; |
32 Addsimps [not_Says_to_self]; |
33 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
33 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |