src/ZF/Update.ML
changeset 6068 2d8f3e1f1151
parent 6048 88e6e55dd168
child 9907 473a6604da94
--- a/src/ZF/Update.ML	Wed Jan 06 15:00:12 1999 +0100
+++ b/src/ZF/Update.ML	Thu Jan 07 10:56:05 1999 +0100
@@ -8,7 +8,7 @@
 
 open Update;
 
-Goal "f(x:=y) ` z = if(z=x, y, f`z)";
+Goal "f(x:=y) ` z = (if z=x then y else f`z)";
 by (simp_tac (simpset() addsimps [update_def]) 1);
 by (case_tac "z : domain(f)" 1);
 by (Asm_simp_tac 1);