[isabelle] Isabelle2013-1-RC3: setup_lifting raises TYPE
When I try to setup lifting for a generic type copy using setup_lifting, I get an
exception TYPE. Here's a minimal example:
theory Copy imports Main begin
typedef 'a copy = "UNIV :: 'a set" ..
Is this on purpose (then I would expect a sensible error message) or a limitation?
This archive was generated by a fusion of
Pipermail (Mailman edition) and