Re: [isabelle] Combining BNF and Quotient
On 03/07/2013 12:58 PM, Makarius wrote:
On Thu, 7 Mar 2013, Ondřej Kunčar wrote:
If you mean the Quotient package by Kaliszyk, Urban, I think you would
have to go to the ML level (which doesn't exist, I know ;)) to setup
the package manually.
Can some of the quotient guys please clarify the situation.
How many quotient packages are there at the moment in Isabelle? Are
there plans to converge them, and remove old stuff?
I know that this is a lot of extra work, but this is how we usually
managed to keep things going (and moving forward) over so many years.
There is one Quotient package and there is Lifting and Transfer, which
almost subsume the functionality of the Quotient package regarding
defining new constants and transferring goals. When Lifting and Transfer
subsume the Quotient package completely, the Quotient package will be
probably outdated and eventually removed. Only the quotient_type command
will be preserved. It's on my todo list but not really on the top
because there are more important things to be done.
As far as I know, the only place where some extra features of the
Quotient package (that are not covered by Lifting and Transfer) are used
This archive was generated by a fusion of
Pipermail (Mailman edition) and