changeset 2451 | ce85a2aafc7a |
parent 2321 | 083912bc5775 |
child 2516 | 4d68fbe6378b |
--- a/src/HOL/Auth/WooLam.ML Thu Dec 19 11:54:19 1996 +0100 +++ b/src/HOL/Auth/WooLam.ML Thu Dec 19 11:58:39 1996 +0100 @@ -96,9 +96,8 @@ (*** Future nonces can't be seen or used! ***) -goal thy "!!evs. evs : woolam ==> \ -\ length evs <= length evt --> \ -\ Nonce (newN evt) ~: parts (sees lost Spy evs)"; +goal thy "!!i. evs : woolam ==> \ +\ length evs <= i --> Nonce(newN(i)) ~: parts (sees lost Spy evs)"; by (parts_induct_tac 1); by (REPEAT_FIRST (fast_tac (!claset addSEs partsEs