Re: [isabelle] Quotient package and the type real


> 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
> (,
> 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


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