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-- |
1 (* Title: HOLCF/fun3.ML
2 ID: $Id$
3 Author: Franz Regensburger
4 Copyright 1993 Technische Universitaet Muenchen
5 *)
7 open Fun3;
9 (* for compatibility with old HOLCF-Version *)
10 qed_goal "inst_fun_pcpo" thy "UU = (%x. UU)"
11 (fn prems =>
12 [
13 (simp_tac (HOL_ss addsimps [UU_def,UU_fun_def]) 1)
14 ]);