equal
deleted
inserted
replaced
182 "" :: "pttrn => patterns" ("_") |
182 "" :: "pttrn => patterns" ("_") |
183 "_patterns" :: "[pttrn, patterns] => patterns" ("_,/ _") |
183 "_patterns" :: "[pttrn, patterns] => patterns" ("_,/ _") |
184 |
184 |
185 translations |
185 translations |
186 "(x, y)" == "CONST Pair x y" |
186 "(x, y)" == "CONST Pair x y" |
|
187 "_pattern x y" => "CONST Pair x y" |
|
188 "_patterns x y" => "CONST Pair x y" |
187 "_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))" |
189 "_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))" |
188 "%(x, y, zs). b" == "CONST prod_case (%x (y, zs). b)" |
190 "%(x, y, zs). b" == "CONST prod_case (%x (y, zs). b)" |
189 "%(x, y). b" == "CONST prod_case (%x y. b)" |
191 "%(x, y). b" == "CONST prod_case (%x y. b)" |
190 "_abs (CONST Pair x y) t" => "%(x, y). t" |
192 "_abs (CONST Pair x y) t" => "%(x, y). t" |
191 -- {* The last rule accommodates tuples in `case C ... (x,y) ... => ...' |
193 -- {* The last rule accommodates tuples in `case C ... (x,y) ... => ...' |