[isabelle] Quotients, lifting and transfer in Isabelle2013-1
I want to learn about the new lifting and transfer tools. Where can I
see simple examples of their use in the HOL development?
For a total quotient I looked at the classic example of Dlists (in
src/HOL/Quotient_Examples/DList.thy), but it seems to be using the old
For an (abstract) type copy I looked at src/HOL/Library/Mapping.thy,
but found it not completely simple due to the use of "option" in the
definition of map.
Thanks for any pointers,
This archive was generated by a fusion of
Pipermail (Mailman edition) and