src/HOLCF/Cprod.thy
changeset 18078 20e5a6440790
parent 18077 f1f4f951ec8d
child 18289 56ddf617d6e8
     1.1 --- a/src/HOLCF/Cprod.thy	Thu Nov 03 01:02:29 2005 +0100
     1.2 +++ b/src/HOLCF/Cprod.thy	Thu Nov 03 01:11:39 2005 +0100
     1.3 @@ -202,20 +202,11 @@
     1.4    "_ctuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(1\<langle>_,/ _\<rangle>)")
     1.5  
     1.6  translations
     1.7 -  "<x, y, z>" == "<x, <y, z>>"
     1.8 -  "<x, y>"    == "cpair$x$y"
     1.9 -
    1.10 -text {* syntax for @{text "LAM <x,y,z>.e"} *}
    1.11 -
    1.12 -syntax
    1.13 -  "_ctuple_pttrn" :: "[pttrn, patterns] => pttrn"  ("<_,/ _>")
    1.14 -
    1.15 -syntax (xsymbols)
    1.16 -  "_ctuple_pttrn" :: "[pttrn, patterns] => pttrn"  ("\<langle>_,/ _\<rangle>")
    1.17 +  "\<langle>x, y, z\<rangle>" == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
    1.18 +  "\<langle>x, y\<rangle>"    == "cpair\<cdot>x\<cdot>y"
    1.19  
    1.20  translations
    1.21 -  "LAM <x,y,zs>. t"       == "csplit$(LAM x <y,zs>. t)"
    1.22 -  "LAM <x,y>. t"          == "csplit$(LAM x y. t)"
    1.23 +  "\<Lambda>(cpair\<cdot>x\<cdot>y). t" == "csplit\<cdot>(\<Lambda> x y. t)"
    1.24  
    1.25  
    1.26  subsection {* Convert all lemmas to the continuous versions *}