[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" ..
setup_lifting type_definition_copy
end

Is this on purpose (then I would expect a sensible error message) or a limitation?

Andreas




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