isabelle: src/HOLCF/Tr2.thy@0a22b9d63a18 (annotated)

1479 21eb5e156d91 expanded tabs clasohm parents: 1168 diff changeset	1	(* Title: HOLCF/tr2.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: 1168 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	Introduce infix if_then_else_fi and boolean connectives andalso, orelse
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	Tr2 = Tr1 +
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	10
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	11	consts
1479 21eb5e156d91 expanded tabs clasohm parents: 1168 diff changeset	12	Icifte :: "tr -> 'c -> 'c -> 'c"
21eb5e156d91 expanded tabs clasohm parents: 1168 diff changeset	13	trand :: "tr -> tr -> tr"
21eb5e156d91 expanded tabs clasohm parents: 1168 diff changeset	14	tror :: "tr -> tr -> tr"
21eb5e156d91 expanded tabs clasohm parents: 1168 diff changeset	15	neg :: "tr -> tr"
752 b89462f9d5f1 ---------------------------------------------------------------------- regensbu parents: 625 diff changeset	16
1479 21eb5e156d91 expanded tabs clasohm parents: 1168 diff changeset	17	syntax "@cifte" :: "tr=>'c=>'c=>'c"
430 89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	18	("(3If _/ (then _/ else _) fi)" 60)
1479 21eb5e156d91 expanded tabs clasohm parents: 1168 diff changeset	19	"@andalso" :: "tr => tr => tr" ("_ andalso _" [36,35] 35)
21eb5e156d91 expanded tabs clasohm parents: 1168 diff changeset	20	"@orelse" :: "tr => tr => tr" ("_ orelse _" [31,30] 30)
752 b89462f9d5f1 ---------------------------------------------------------------------- regensbu parents: 625 diff changeset	21
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 752 diff changeset	22	translations "x andalso y" == "trand`x`y"
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 752 diff changeset	23	"x orelse y" == "tror`x`y"
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 752 diff changeset	24	"If b then e1 else e2 fi" == "Icifte`b`e1`e2"
625 119391dd1d59 New version nipkow parents: 430 diff changeset	25
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 752 diff changeset	26	defs
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	27
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 752 diff changeset	28	ifte_def "Icifte == (LAM t e1 e2.tr_when`e1`e2`t)"
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 752 diff changeset	29	andalso_def "trand == (LAM t1 t2.tr_when`t2`FF`t1)"
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 752 diff changeset	30	orelse_def "tror == (LAM t1 t2.tr_when`TT`t2`t1)"
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 752 diff changeset	31	neg_def "neg == (LAM t. tr_when`FF`TT`t)"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	32
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	33	end

author	paulson
	Mon, 23 Sep 1996 18:18:18 +0200
changeset 2010	0a22b9d63a18
parent 1479	21eb5e156d91
permissions	-rw-r--r--