Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Auth/WooLam.ML
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
isabelle