Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Added ability to have case expressions involving tuples. (via translation)
authornipkow
Thu, 17 Apr 1997 17:54:21 +0200
changeset 2973 184c7cd8043d
parent 2972 11e124d2e184
child 2974 bb55cab416af
Added ability to have case expressions involving tuples. (via translation)
src/HOL/Prod.thy file | annotate | diff | comparison | revisions 
--- 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)"
isabelle