# HG changeset patch
# User nipkow
# Date 861292461 -7200
# Node ID 184c7cd8043d6dcdbd0fca2d57fbc28947a5326b
# Parent  11e124d2e1842615eceb1a7a46a1f8f7bdab05c8
Added ability to have case expressions involving tuples. (via translation)

diff -r 11e124d2e184 -r 184c7cd8043d src/HOL/Prod.thy
--- a/src/HOL/Prod.thy	Thu Apr 17 14:41:56 1997 +0200
+++ b/src/HOL/Prod.thy	Thu Apr 17 17:54:21 1997 +0200
@@ -44,9 +44,10 @@
 syntax
   "@Tuple"      :: "['a, args] => 'a * 'b"      ("(1'(_,/ _'))")
 
-  "@pttrn"      :: [pttrn, pttrns] => pttrn     ("'(_,/_')")
+  "_pttrn"      :: [pttrn, pttrns] => pttrn     ("'(_,/_')")
   ""            :: pttrn => pttrns              ("_")
-  "@pttrns"     :: [pttrn, pttrns] => pttrns    ("_,/_")
+  "_pttrns"     :: [pttrn, pttrns] => pttrns    ("_,/_")
+
   "@Sigma"      :: "[idt, 'a set, 'b set] => ('a * 'b) set"     ("(3SIGMA _:_./ _)" 10)
   "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    ("_ Times _" [81, 80] 80)
 
@@ -56,6 +57,9 @@
 
   "%(x,y,zs).b" == "split(%x (y,zs).b)"
   "%(x,y).b"    == "split(%x y.b)"
+  "_abs (Pair x y) t" => "%(x,y).t"
+  (* The last rule accommodates tuples in `case C ... (x,y) ... => ...'
+     The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *)
 
   "SIGMA x:A.B" => "Sigma A (%x.B)"
   "A Times B"   => "Sigma A (_K B)"