Re: [isabelle] State of the State Monad

Excellent, thanks!


On 12 July 2017 14:50:38 CEST, Andreas Lochbihler <andreas.lochbihler at> wrote:
>Hi Lars,
>I've ported the tree relabelling (AFP/6a4641399c0a). I had to prove a
>bunch of lemmas 
>about how the state monad operations interact. They are at the top of 
>Tree_Relabelling.thy, but you might want to move them to State_Monad in
>On 12/07/17 06:03, Lars Hupel wrote:
>>> Good point. If nobody objects I'll do that later this week. I was
>>> planning to clean up some stuff in the vicinity ("Finite_Map")
>> See now Isabelle/d157195a468a and AFP/9f41cb6d9cfa.
>> I'll leave the porting of the tree relabeling to you, Andreas :-)
>> Cheers
>> Lars

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.