src/HOLCF/Fun3.ML

Conversion of HyperNat to Isar format and its declaration as a semiring

(*  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";