> thanks for the reminder. Cf. c6714a9562ae and a5a24e1a6d6f. Great, thanks!
> 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. Cheers Lars _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
