Re: [isabelle] Quotient package and the type real



Dmitriy,

> Hello Filip,
>
> I cannot say anything about the descending method, but your example works
> fine with Lifting and Transfer in Isabelle 2013 (see below). And since there
> are plans to eventually remove the Quotient package
> (https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-March/msg00026.html),
> I would recommend to use these more recent tools.

I have successfully migrated my formalization - it was quite easy to
do, and everything works fine now. Thank you very much for your
advice!

Filip!




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