src/HOLCF/Fun3.ML
author berghofe
Fri, 11 Jul 2003 14:55:17 +0200
changeset 14102 8af7334af4b3
parent 12030 46d57d0290a2
child 14981 e73f8140af78
permissions -rw-r--r--
- Installed specific code generator for equality enforcing that arguments do not have function types, which would result in an error message during compilation. - Added test case generators for basic types.

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