[isabelle-dev] map/rel/set for lift_bnf
hupel at in.tum.de
Wed Jul 12 08:17:43 CEST 2017
> thanks for the reminder. Cf. c6714a9562ae and a5a24e1a6d6f.
> Note that this still doesn’t provide the interface to Lifting and Transfer via transfer rules for the BNF constants (which is more complicated since lift_bnf doesn’t know about Lifting, in particular about the correspondence relations).
That's fair enough. The proofs are not that complicated.
More information about the isabelle-dev