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.
swapped condition in update_apply.
authornipkow
Mon, 13 Jul 1998 16:04:22 +0200
changeset 5133 42a7fe39a63a
parent 5132 24f992a25adc
child 5134 51f81581e3d9
swapped condition in update_apply.
src/HOL/Update.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Update.ML	Sun Jul 12 11:49:17 1998 +0200
+++ b/src/HOL/Update.ML	Mon Jul 13 16:04:22 1998 +0200
@@ -20,7 +20,7 @@
 
 AddIffs [refl RS update_idem];
 
-Goal "(f(x:=y))z = (if x=z then y else f z)";
+Goal "(f(x:=y))z = (if z=x then y else f z)";
 by (simp_tac (simpset() addsimps [update_def]) 1);
 qed "update_apply";
 Addsimps [update_apply];
isabelle