src/HOL/Update.ML
changeset 5133 42a7fe39a63a
parent 5070 c42429b3e2f2
child 5154 40fd46f3d3a1
--- 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];