Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
deleted redundant quantifiers
authorpaulson
Wed, 16 Sep 1998 10:28:54 +0200
changeset 5493 e335c51808ac
parent 5492 d9fc3457554e
child 5494 2df1a9d43e3c
deleted redundant quantifiers
src/HOL/Auth/Message.ML file | annotate | diff | comparison | revisions 
--- 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));
isabelle