| 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];