changeset 3842 | b55686a7b22c |
parent 2640 | ee4dfce170a0 |
child 9245 | 428385c4bc50 |
--- a/src/HOLCF/Fun3.ML Fri Oct 10 18:37:49 1997 +0200 +++ b/src/HOLCF/Fun3.ML Fri Oct 10 19:02:28 1997 +0200 @@ -7,7 +7,7 @@ open Fun3; (* for compatibility with old HOLCF-Version *) -qed_goal "inst_fun_pcpo" thy "UU = (%x.UU)" +qed_goal "inst_fun_pcpo" thy "UU = (%x. UU)" (fn prems => [ (simp_tac (HOL_ss addsimps [UU_def,UU_fun_def]) 1)