changeset 2493 | bdeb5024353a |
parent 2469 | b50b8c0eec01 |
child 2496 | 40efb87985b5 |
--- a/src/ZF/AC/Cardinal_aux.ML Wed Jan 08 15:03:53 1997 +0100 +++ b/src/ZF/AC/Cardinal_aux.ML Wed Jan 08 15:04:27 1997 +0100 @@ -69,7 +69,7 @@ setloop (split_tac [expand_if] ORELSE' etac UnE); goal upair.thy "{x, y} - {y} = {x} - {y}"; -by (fast_tac eq_cs 1); +by (Fast_tac 1); val double_Diff_sing = result(); goal upair.thy "if({y,z}-{z}=0, z, THE w. {y,z}-{z}={w}) = y";