equal
deleted
inserted
replaced
32 (**** Inductive proofs about yahalom ****) |
32 (**** Inductive proofs about yahalom ****) |
33 |
33 |
34 (*Nobody sends themselves messages*) |
34 (*Nobody sends themselves messages*) |
35 goal thy "!!evs. evs: yahalom ==> ALL A X. Says A A X ~: set evs"; |
35 goal thy "!!evs. evs: yahalom ==> ALL A X. Says A A X ~: set evs"; |
36 by (etac yahalom.induct 1); |
36 by (etac yahalom.induct 1); |
37 by (Auto_tac()); |
37 by Auto_tac; |
38 qed_spec_mp "not_Says_to_self"; |
38 qed_spec_mp "not_Says_to_self"; |
39 Addsimps [not_Says_to_self]; |
39 Addsimps [not_Says_to_self]; |
40 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
40 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
41 |
41 |
42 |
42 |