--- a/src/HOLCF/Cprod3.thy Mon Sep 22 17:31:57 1997 +0200
+++ b/src/HOLCF/Cprod3.thy Mon Sep 22 17:35:52 1997 +0200
@@ -3,8 +3,7 @@
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Class instance of * for class pcpo
-
+Class instance of * for class pcpo and cpo.
*)
Cprod3 = Cprod2 +
@@ -12,16 +11,16 @@
instance "*" :: (cpo,cpo)cpo (cpo_cprod)
instance "*" :: (pcpo,pcpo)pcpo (least_cprod)
-consts
- cpair :: "'a -> 'b -> ('a*'b)" (* continuous pairing *)
+consts
+ cpair :: "'a -> 'b -> ('a*'b)" (* continuous pairing *)
cfst :: "('a*'b)->'a"
csnd :: "('a*'b)->'b"
csplit :: "('a->'b->'c)->('a*'b)->'c"
-syntax
+syntax
"@ctuple" :: "['a, args] => 'a * 'b" ("(1<_,/ _>)")
-translations
+translations
"<x, y, z>" == "<x, <y, z>>"
"<x, y>" == "cpair`x`y"
@@ -42,41 +41,38 @@
LAM <x,y,z>.e
*)
-types
- Cletbinds Cletbind
+constdefs
+ CLet :: "'a -> ('a -> 'b) -> 'b"
+ "CLet == LAM s f.f`s"
+
-consts
- CLet :: "'a -> ('a -> 'b) -> 'b"
+(* syntax for Let *)
+
+types
+ Cletbinds Cletbind
syntax
- (* syntax for Let *)
-
"_Cbind" :: "[pttrn, 'a] => Cletbind" ("(2_ =/ _)" 10)
"" :: "Cletbind => Cletbinds" ("_")
"_Cbinds" :: "[Cletbind, Cletbinds] => Cletbinds" ("_;/ _")
- "_CLet" :: "[Cletbinds, 'a] => 'a" ("(Let (_)/ in (_))" 10)
+ "_CLet" :: "[Cletbinds, 'a] => 'a" ("(Let (_)/ in (_))" 10)
translations
- (* translation for Let *)
"_CLet (_Cbinds b bs) e" == "_CLet b (_CLet bs e)"
"Let x = a in e" == "CLet`a`(LAM x.e)"
-defs
- (* Misc Definitions *)
- CLet_def "CLet == LAM s. LAM f.f`s"
+
+(* syntax for LAM <x,y,z>.e *)
syntax
- (* syntax for LAM <x,y,z>.E *)
- "@Cpttrn" :: "[pttrn,pttrns] => pttrn" ("<_,/_>")
+ "_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)" ("(3LAM <_>./ _)" [0, 10] 10)
translations
- (* translations for LAM <x,y,z>.E *)
- "LAM <x,y,zs>.b" == "csplit`(LAM x.LAM <y,zs>.b)"
- "LAM <x,y>.b" == "csplit`(LAM x.LAM y.b)"
- (* reverse translation <= does not work yet !! *)
+ "LAM <x,y,zs>.b" == "csplit`(LAM x. LAM <y,zs>.b)"
+ "LAM <x,y>. LAM zs. b" <= "csplit`(LAM x y zs. b)"
+ "LAM <x,y>.b" == "csplit`(LAM x y. b)"
+
+syntax (symbols)
+ "_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)" ("(3\\<Lambda><_>./ _)" [0, 10] 10)
end
-
-
-
-