src/HOLCF/Fun3.ML
author paulson
Tue Jul 04 15:58:11 2000 +0200 (2000-07-04)
changeset 9245 428385c4bc50
parent 3842 b55686a7b22c
child 9248 e1dee89de037
permissions -rw-r--r--
removed most batch-style proofs
paulson@9245
     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
slotosch@2640
     7
(* for compatibility with old HOLCF-Version *)
paulson@9245
     8
val prems = goal thy "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";