src/HOL/Nominal/Examples/Fsub.thy
changeset 61069 aefe89038dd2
parent 58305 57752a91eec4
child 63167 0909deb8059b
     1.1 --- a/src/HOL/Nominal/Examples/Fsub.thy	Mon Aug 31 20:56:24 2015 +0200
     1.2 +++ b/src/HOL/Nominal/Examples/Fsub.thy	Mon Aug 31 21:01:21 2015 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  section {* Types for Names, Nominal Datatype Declaration for Types and Terms *}
     1.5  
     1.6  no_syntax
     1.7 -  "_Map" :: "maplets => 'a ~=> 'b"  ("(1[_])")
     1.8 +  "_Map" :: "maplets => 'a \<rightharpoonup> 'b"  ("(1[_])")
     1.9  
    1.10  text {* The main point of this solution is to use names everywhere (be they bound, 
    1.11    binding or free). In System \FSUB{} there are two kinds of names corresponding to