replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style
(* Title: HOLCF/Fun3.ML
ID: $Id$
Author: Franz Regensburger
License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
(* for compatibility with old HOLCF-Version *)
Goal "UU = (%x. UU)";
by (simp_tac (HOL_ss addsimps [UU_def,UU_fun_def]) 1);
qed "inst_fun_pcpo";