Added ability to have case expressions involving tuples. (via translation)
1.1 --- a/src/HOL/Prod.thy Thu Apr 17 14:41:56 1997 +0200
1.2 +++ b/src/HOL/Prod.thy Thu Apr 17 17:54:21 1997 +0200
1.3 @@ -44,9 +44,10 @@
1.4 syntax
1.5 "@Tuple" :: "['a, args] => 'a * 'b" ("(1'(_,/ _'))")
1.6
1.7 - "@pttrn" :: [pttrn, pttrns] => pttrn ("'(_,/_')")
1.8 + "_pttrn" :: [pttrn, pttrns] => pttrn ("'(_,/_')")
1.9 "" :: pttrn => pttrns ("_")
1.10 - "@pttrns" :: [pttrn, pttrns] => pttrns ("_,/_")
1.11 + "_pttrns" :: [pttrn, pttrns] => pttrns ("_,/_")
1.12 +
1.13 "@Sigma" :: "[idt, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" 10)
1.14 "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ Times _" [81, 80] 80)
1.15
1.16 @@ -56,6 +57,9 @@
1.17
1.18 "%(x,y,zs).b" == "split(%x (y,zs).b)"
1.19 "%(x,y).b" == "split(%x y.b)"
1.20 + "_abs (Pair x y) t" => "%(x,y).t"
1.21 + (* The last rule accommodates tuples in `case C ... (x,y) ... => ...'
1.22 + The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *)
1.23
1.24 "SIGMA x:A.B" => "Sigma A (%x.B)"
1.25 "A Times B" => "Sigma A (_K B)"