author | haftmann |
Sun, 06 Sep 2015 22:14:37 +0200 | |
changeset 61122 | af67ed04da64 |
parent 61121 | efe8b18306b7 |
child 61123 | a1141fb798ff |
--- a/src/HOL/Product_Type.thy Sun Sep 06 21:55:13 2015 +0200 +++ b/src/HOL/Product_Type.thy Sun Sep 06 22:14:37 2015 +0200 @@ -307,11 +307,6 @@ "%(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" - - - - - -- \<open>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\<close>