| changeset 1267 | bca91b4e1710 |
| parent 1043 | ffa68eb2730b |
| child 1461 | 6bcb44e4d6e5 |
--- a/src/HOLCF/Pcpo.ML Wed Oct 04 13:12:14 1995 +0100 +++ b/src/HOLCF/Pcpo.ML Wed Oct 04 14:01:44 1995 +0100 @@ -105,7 +105,7 @@ (atac 1), (res_inst_tac [("s","Y(Suc(x))"),("t","X(Suc(x))")] subst 1), (rtac sym 1), - (asm_simp_tac nat_ss 1), + (Asm_simp_tac 1), (rtac is_ub_thelub 1), (resolve_tac prems 1) ]);