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.
Had to remove {x.x=a} = a from !simpset in one proof.
authornipkow
Fri, 01 Aug 1997 09:41:38 +0200
changeset 3583 5a47b869d16a
parent 3582 b87c86b6c291
child 3584 8f9ee0f79d9a
Had to remove {x.x=a} = a from !simpset in one proof.
src/HOL/Auth/Message.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Auth/Message.ML	Fri Aug 01 09:39:28 1997 +0200
+++ b/src/HOL/Auth/Message.ML	Fri Aug 01 09:41:38 1997 +0200
@@ -524,7 +524,7 @@
 
 
 goal thy "!!H. analz H = analz H' ==> analz(insert X H) = analz(insert X H')";
-by (asm_simp_tac (!simpset addsimps [insert_def] 
+by (asm_simp_tac (!simpset addsimps [insert_def] delsimps [singleton_conv]
                            setloop (rtac analz_cong)) 1);
 qed "analz_insert_cong";
isabelle