src/HOLCF/Fun3.ML
author wenzelm
Sat Nov 03 01:41:26 2001 +0100 (2001-11-03)
changeset 12030 46d57d0290a2
parent 9248 e1dee89de037
child 14981 e73f8140af78
permissions -rw-r--r--
GPLed;
paulson@9245
     1
(*  Title:      HOLCF/Fun3.ML
nipkow@243
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Franz Regensburger
wenzelm@12030
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
nipkow@243
     5
*)
nipkow@243
     6
slotosch@2640
     7
(* for compatibility with old HOLCF-Version *)
paulson@9248
     8
Goal "UU = (%x. UU)";
paulson@9245
     9
by (simp_tac (HOL_ss addsimps [UU_def,UU_fun_def]) 1);
paulson@9245
    10
qed "inst_fun_pcpo";