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.
Removed image_eqI from simpset because of clash with neq_shrK.
authornipkow
Fri, 17 Oct 1997 09:03:16 +0200
changeset 3908 4f19a40a9343
parent 3907 51c00e87bd6e
child 3909 e48e2fb8b895
Removed image_eqI from simpset because of clash with neq_shrK.
src/HOL/Auth/Shared.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Auth/Shared.ML	Thu Oct 16 16:54:31 1997 +0200
+++ b/src/HOL/Auth/Shared.ML	Fri Oct 17 09:03:16 1997 +0200
@@ -87,7 +87,7 @@
 qed "shrK_neq";
 
 Addsimps [Key_not_used, shrK_neq, shrK_neq RS not_sym];
-
+Delsimps [image_eqI]; (* loops together with shrK_neq *)
 
 (*** Fresh nonces ***)
isabelle