# HG changeset patch # User haftmann # Date 1441570491 -7200 # Node ID e70daf0d0fad2b61ea4d1247dff1dd9cc1f35e88 # Parent a1141fb798ff98a35ba89af0514f129e9e039d9f tuned diff -r a1141fb798ff -r e70daf0d0fad src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Sun Sep 06 22:14:39 2015 +0200 +++ b/src/HOL/Product_Type.thy Sun Sep 06 22:14:51 2015 +0200 @@ -300,15 +300,16 @@ "_patterns" :: "[pttrn, patterns] => patterns" ("_,/ _") translations - "(x, y)" == "CONST Pair x y" - "_pattern x y" => "CONST Pair x y" - "_patterns x y" => "CONST Pair x y" - "_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))" - "%(x, y, zs). b" == "CONST case_prod (%x (y, zs). b)" - "%(x, y). b" == "CONST case_prod (%x y. b)" - "_abs (CONST 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\ + "(x, y)" \ "CONST Pair x y" + "_pattern x y" \ "CONST Pair x y" + "_patterns x y" \ "CONST Pair x y" + "_tuple x (_tuple_args y z)" \ "_tuple x (_tuple_arg (_tuple y z))" + "\(x, y, zs). b" \ "CONST case_prod (\x (y, zs). b)" + "\(x, y). b" \ "CONST case_prod (\x y. b)" + "_abs (CONST Pair x y) t" \ "\(x, y). t" + -- \This rule accommodates tuples in @{text "case C \ (x, y) \ \ \"}: + The @{text "(x, y)"} is parsed as @{text "Pair x y"} because it is @{text logic}, + not @{text pttrn}.\ (* print "split f" as "\(x,y). f x y" and "split (\x. f x)" as "\(x,y). f x y" *) typed_print_translation \