src/HOLCF/Fun3.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 3842 b55686a7b22c
child 9245 428385c4bc50
permissions -rw-r--r--
made tutorial first;
clasohm@1461
     1
(*  Title:      HOLCF/fun3.ML
nipkow@243
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Franz Regensburger
nipkow@243
     4
    Copyright   1993 Technische Universitaet Muenchen
nipkow@243
     5
*)
nipkow@243
     6
nipkow@243
     7
open Fun3;
slotosch@2640
     8
slotosch@2640
     9
(* for compatibility with old HOLCF-Version *)
wenzelm@3842
    10
qed_goal "inst_fun_pcpo" thy "UU = (%x. UU)"
slotosch@2640
    11
 (fn prems => 
slotosch@2640
    12
        [
slotosch@2640
    13
        (simp_tac (HOL_ss addsimps [UU_def,UU_fun_def]) 1)
slotosch@2640
    14
        ]);