author | paulson |
Wed, 16 Sep 1998 10:28:54 +0200 | |
changeset 5493 | e335c51808ac |
parent 5492 | d9fc3457554e |
child 5494 | 2df1a9d43e3c |
--- a/src/HOL/Auth/Message.ML Tue Sep 15 15:10:38 1998 +0200 +++ b/src/HOL/Auth/Message.ML Wed Sep 16 10:28:54 1998 +0200 @@ -33,7 +33,7 @@ (** Inverse of keys **) -Goal "!!K K'. (invKey K = invKey K') = (K=K')"; +Goal "(invKey K = invKey K') = (K=K')"; by Safe_tac; by (rtac box_equals 1); by (REPEAT (rtac invKey 2));