| changeset 61069 | aefe89038dd2 |
| parent 60580 | 7e741e22d7fc |
| child 61166 | 5976fe402824 |
--- a/src/HOL/Nominal/Examples/Pattern.thy Mon Aug 31 20:56:24 2015 +0200 +++ b/src/HOL/Nominal/Examples/Pattern.thy Mon Aug 31 21:01:21 2015 +0200 @@ -5,7 +5,7 @@ begin no_syntax - "_Map" :: "maplets => 'a ~=> 'b" ("(1[_])") + "_Map" :: "maplets => 'a \<rightharpoonup> 'b" ("(1[_])") atom_decl name