isabelle: src/HOLCF/Holcfb.thy@23ceb1dc9755 (annotated)

243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	1	(* Title: HOLCF/holcfb.thy
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	2	ID: $Id$
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	3	Author: Franz Regensburger
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	Basic definitions for the embedding of LCF into HOL.
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	7
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	8	*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	9
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	10	Holcfb = Nat +
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	11
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	12	consts
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: 1168 diff changeset	13	theleast :: "(nat=>bool)=>nat"
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 243 diff changeset	14	defs
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	15
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 243 diff changeset	16	theleast_def "theleast P == (@z.(P z & (!n.P n --> z<=n)))"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	17
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: 1168 diff changeset	18	(* start 8bit 1 *)
ea0668a1c0ba added 8bit pragmas regensbu parents: 1168 diff changeset	19	(* end 8bit 1 *)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	20
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: 1168 diff changeset	21	end

author	paulson
	Thu, 18 Jan 1996 10:38:29 +0100
changeset 1444	23ceb1dc9755
parent 1274	ea0668a1c0ba
child 1479	21eb5e156d91
permissions	-rw-r--r--