> 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
That's fair enough. The proofs are not that complicated.
isabelle-dev mailing list