Re: [isabelle] State of the State Monad



Excellent, thanks!

Cheers
Lars

On 12 July 2017 14:50:38 CEST, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> 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
>HOL/Library.
>
>Cheers,
>Andreas
>
>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")
>anyway.
>> 
>> 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.