# HG changeset patch
# User wenzelm
# Date 874942552 -7200
# Node ID 37aa547fb5640bc72dbb2284ff5fc6cdb354e996
# Parent  9f9bcce140ce02146d0b80dd6e0a5770a33d0ea3
fixed LAM <x,y,zs>.b syntax (may break some unusual cases);

diff -r 9f9bcce140ce -r 37aa547fb564 src/HOLCF/Cprod3.thy
--- 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
-
-
-
-