equal
deleted
inserted
replaced
31 by (REPEAT (resolve_tac [exI,bexI] 1)); |
31 by (REPEAT (resolve_tac [exI,bexI] 1)); |
32 by (rtac (kerberos_ban.Nil RS kerberos_ban.Kb1 RS kerberos_ban.Kb2 RS |
32 by (rtac (kerberos_ban.Nil RS kerberos_ban.Kb1 RS kerberos_ban.Kb2 RS |
33 kerberos_ban.Kb3 RS kerberos_ban.Kb4) 2); |
33 kerberos_ban.Kb3 RS kerberos_ban.Kb4) 2); |
34 by possibility_tac; |
34 by possibility_tac; |
35 by (ALLGOALS Asm_simp_tac); |
35 by (ALLGOALS Asm_simp_tac); |
36 by (ALLGOALS trans_tac); |
|
37 result(); |
36 result(); |
38 |
37 |
39 |
38 |
40 |
39 |
41 (**** Inductive proofs about kerberos_ban ****) |
40 (**** Inductive proofs about kerberos_ban ****) |