isabelle: src/HOLCF/Fun3.ML@36bfceef1800 (annotated)

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 243 diff changeset	1	(* Title: HOLCF/fun3.ML
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	2	ID: $Id$
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 243 diff changeset	3	Author: Franz Regensburger
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	4	Copyright 1993 Technische Universitaet Muenchen
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	5	*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	6
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	7	open Fun3;
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 1461 diff changeset	8
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 1461 diff changeset	9	(* for compatibility with old HOLCF-Version *)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 1461 diff changeset	10	qed_goal "inst_fun_pcpo" thy "UU = (%x.UU)"
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 1461 diff changeset	11	(fn prems =>
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 1461 diff changeset	12	[
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 1461 diff changeset	13	(simp_tac (HOL_ss addsimps [UU_def,UU_fun_def]) 1)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 1461 diff changeset	14	]);

author	paulson
	Thu, 15 May 1997 12:53:12 +0200
changeset 3194	36bfceef1800
parent 2640	ee4dfce170a0
child 3842	b55686a7b22c
permissions	-rw-r--r--