src/HOL/Prod.thy
changeset 1114 c8dfb56a7e95
parent 1081 884c6ef06fbf
child 1273 6960ec882bca
     1.1 --- a/src/HOL/Prod.thy	Tue May 09 10:43:19 1995 +0200
     1.2 +++ b/src/HOL/Prod.thy	Tue May 09 22:10:08 1995 +0200
     1.3 @@ -40,16 +40,16 @@
     1.4  syntax
     1.5    "@Tuple"      :: "['a, args] => 'a * 'b"            ("(1'(_,/ _'))")
     1.6  
     1.7 -  "@pttrn"  :: "pttrns => pttrn"            ("'(_')")
     1.8 -  ""        :: " pttrn           => pttrns" ("_")
     1.9 -  "@pttrns" :: "[pttrn,pttrns]   => pttrns" ("_,/_")
    1.10 +  "@pttrn"  :: "[pttrn,pttrns] => pttrn"              ("'(_,/_')")
    1.11 +  ""        :: " pttrn         => pttrns"             ("_")
    1.12 +  "@pttrns" :: "[pttrn,pttrns] => pttrns"             ("_,/_")
    1.13  
    1.14  translations
    1.15    "(x, y, z)"   == "(x, (y, z))"
    1.16    "(x, y)"      == "Pair x y"
    1.17  
    1.18 -  "%(x,y,zs).b"   => "split(%x (y,zs).b)"
    1.19 -  "%(x,y).b"      => "split(%x y.b)"
    1.20 +  "%(x,y,zs).b"   == "split(%x (y,zs).b)"
    1.21 +  "%(x,y).b"      == "split(%x y.b)"
    1.22  (* The <= direction fails if split has more than one argument because
    1.23     ast-matching fails. Otherwise it would work fine *)
    1.24  
    1.25 @@ -75,12 +75,12 @@
    1.26    Unity_def     "() == Abs_Unit(True)"
    1.27  
    1.28  end
    1.29 -
    1.30 +(*
    1.31  ML
    1.32  
    1.33  local open Syntax
    1.34  
    1.35 -fun pttrn s = const"@pttrn" $ s;
    1.36 +fun pttrn(_ $ s $ t) = const"@pttrn" $ s $ t;
    1.37  fun pttrns s t = const"@pttrns" $ s $ t;
    1.38  
    1.39  fun split2(Abs(x,T,t)) =
    1.40 @@ -102,3 +102,4 @@
    1.41  val print_translation = [("split", split_tr')];
    1.42  
    1.43  end;
    1.44 +*)