isabelle: src/HOLCF/Fun3.ML@1ca01fc3cca1 (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 *)
3842 b55686a7b22c fixed dots; wenzelm parents: 2640 diff changeset	10	qed_goal "inst_fun_pcpo" thy "UU = (%x. UU)"
2640 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
	Mon, 24 May 1999 15:48:27 +0200
changeset 6709	1ca01fc3cca1
parent 3842	b55686a7b22c
child 9245	428385c4bc50
permissions	-rw-r--r--