equal
deleted
inserted
replaced
127 by (rtac selectI 1); |
127 by (rtac selectI 1); |
128 by (Fast_tac 1); |
128 by (Fast_tac 1); |
129 qed "Nonce_supply"; |
129 qed "Nonce_supply"; |
130 |
130 |
131 (*Tactic for possibility theorems*) |
131 (*Tactic for possibility theorems*) |
132 val possibility_tac = |
132 fun possibility_tac st = st |> |
133 REPEAT (*omit used_Says so that Nonces, Keys start from different traces!*) |
133 REPEAT (*omit used_Says so that Nonces, Keys start from different traces!*) |
134 (ALLGOALS (simp_tac (!simpset delsimps [used_Says] setSolver safe_solver)) |
134 (ALLGOALS (simp_tac (!simpset delsimps [used_Says] setSolver safe_solver)) |
135 THEN |
135 THEN |
136 REPEAT_FIRST (eq_assume_tac ORELSE' |
136 REPEAT_FIRST (eq_assume_tac ORELSE' |
137 resolve_tac [refl, conjI, Nonce_supply])); |
137 resolve_tac [refl, conjI, Nonce_supply])); |