isabelle: src/HOLCF/Sprod3.thy@46d57d0290a2 (annotated)

1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	1	(* Title: HOLCF/sprod3.thy
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	2	ID: $Id$
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	3	Author: Franz Regensburger
12030 46d57d0290a2 GPLed; wenzelm parents: 10834 diff changeset	4	License: GPL (GNU GENERAL PUBLIC LICENSE)
243 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	Class instance of ** for class pcpo
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	Sprod3 = Sprod2 +
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	10
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2420 diff changeset	11	instance "**" :: (pcpo,pcpo)pcpo (least_sprod,cpo_sprod)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	12
752 b89462f9d5f1 ---------------------------------------------------------------------- regensbu parents: 657 diff changeset	13	consts
2394 91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	14	spair :: "'a -> 'b -> ('a*'b)" ( continuous strict pairing *)
91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	15	sfst :: "('a**'b)->'a"
91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	16	ssnd :: "('a**'b)->'b"
91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	17	ssplit :: "('a->'b->'c)->('a**'b)->'c"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	18
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 752 diff changeset	19	syntax
5033 06f03dc5a1dc changed (\| \|) syntax to (: :); wenzelm parents: 3842 diff changeset	20	"@stuple" :: "['a, args] => 'a ** 'b" ("(1'(:_,/ _:'))")
752 b89462f9d5f1 ---------------------------------------------------------------------- regensbu parents: 657 diff changeset	21
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 752 diff changeset	22	translations
5033 06f03dc5a1dc changed (\| \|) syntax to (: :); wenzelm parents: 3842 diff changeset	23	"(:x, y, z:)" == "(:x, (:y, z:):)"
10834 a7897aebbffc * empty log message * nipkow parents: 5033 diff changeset	24	"(:x, y:)" == "spair$x$y"
625 119391dd1d59 New version nipkow parents: 442 diff changeset	25
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 752 diff changeset	26	defs
3842 b55686a7b22c fixed dots; wenzelm parents: 2763 diff changeset	27	spair_def "spair == (LAM x y. Ispair x y)"
b55686a7b22c fixed dots; wenzelm parents: 2763 diff changeset	28	sfst_def "sfst == (LAM p. Isfst p)"
b55686a7b22c fixed dots; wenzelm parents: 2763 diff changeset	29	ssnd_def "ssnd == (LAM p. Issnd p)"
10834 a7897aebbffc * empty log message * nipkow parents: 5033 diff changeset	30	ssplit_def "ssplit == (LAM f. strictify$(LAM p. f$(sfst$p)$(ssnd$p)))"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	31
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	32	end

author	wenzelm
	Sat, 03 Nov 2001 01:41:26 +0100
changeset 12030	46d57d0290a2
parent 10834	a7897aebbffc
child 14981	e73f8140af78
permissions	-rw-r--r--