don't use the human-readable version of the rsp thm as a goal in the ML interface (there is no formal definition of its statement); make tactics more robust wrt. predicates in predicators; tuned

go back to the complicated code equation registration (because of type classes) that was lost in 922586b1bc87; make it even more hackish to get which code equation was used

Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype

tuned proof; forget the transfer rule for size_fset

return also which code equation was used; tuned

publish lifting_forget and lifting_udpate interface

note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional

export the result of lifting_def

useful function

parametrize liting of terms by quotients