equal
deleted
inserted
replaced
140 by (Blast_tac 1); |
140 by (Blast_tac 1); |
141 qed "Nonce_supply1"; |
141 qed "Nonce_supply1"; |
142 |
142 |
143 Goal "Nonce (@ N. Nonce N ~: used evs) ~: used evs"; |
143 Goal "Nonce (@ N. Nonce N ~: used evs) ~: used evs"; |
144 by (rtac (lemma RS exE) 1); |
144 by (rtac (lemma RS exE) 1); |
145 by (rtac selectI 1); |
145 by (rtac someI 1); |
146 by (Fast_tac 1); |
146 by (Fast_tac 1); |
147 qed "Nonce_supply"; |
147 qed "Nonce_supply"; |
148 |
148 |
149 (*Tactic for possibility theorems*) |
149 (*Tactic for possibility theorems*) |
150 fun possibility_tac st = st |> |
150 fun possibility_tac st = st |> |