| changeset 5983 | 79e301a6a51b |
| parent 5493 | e335c51808ac |
| child 6141 | a6922171b396 |
--- a/src/HOL/Auth/Message.ML Fri Nov 27 16:54:59 1998 +0100 +++ b/src/HOL/Auth/Message.ML Fri Nov 27 17:00:30 1998 +0100 @@ -314,7 +314,7 @@ by (blast_tac (claset() addSEs [add_leE]) 2); (*Nonce case*) by (res_inst_tac [("x","N + Suc nat")] exI 1); -by (fast_tac (claset() addSEs [add_leE] addaltern ("trans_tac",trans_tac)) 1); +by (auto_tac (claset() addSEs [add_leE], simpset())); qed "msg_Nonce_supply";