src/HOL/IMPP/Com.thy
changeset 61069 aefe89038dd2
parent 60754 02924903a6fd
child 63167 0909deb8059b
     1.1 --- a/src/HOL/IMPP/Com.thy	Mon Aug 31 20:56:24 2015 +0200
     1.2 +++ b/src/HOL/IMPP/Com.thy	Mon Aug 31 21:01:21 2015 +0200
     1.3 @@ -43,7 +43,7 @@
     1.4  
     1.5  consts bodies :: "(pname  *  com) list"(* finitely many procedure definitions *)
     1.6  definition
     1.7 -  body :: " pname ~=> com" where
     1.8 +  body :: " pname \<rightharpoonup> com" where
     1.9    "body = map_of bodies"
    1.10  
    1.11