changeset 9248 | e1dee89de037 |
parent 9245 | 428385c4bc50 |
child 12030 | 46d57d0290a2 |
--- a/src/HOLCF/Fun3.ML Wed Jul 05 14:26:58 2000 +0200 +++ b/src/HOLCF/Fun3.ML Wed Jul 05 16:37:52 2000 +0200 @@ -5,6 +5,6 @@ *) (* for compatibility with old HOLCF-Version *) -val prems = goal thy "UU = (%x. UU)"; +Goal "UU = (%x. UU)"; by (simp_tac (HOL_ss addsimps [UU_def,UU_fun_def]) 1); qed "inst_fun_pcpo";