[isabelle-dev] Acces to internal interfaces ...

[Burkhart Wolff]

Dear all,

in Isabelle 2016, certain traditional interfaces to data-type packages
do no longer exist, for example Datatype.get_info thy typename or
its homologue on records. This function yielded for a given typename 
the list of constructors together with their types, and other information.

This change is, as I assume, a consequence of the new layer of type-related
packages of more recent isabelle versions.

One can, of course, extract this information from the type-exhaustion schemes.
Is there another recommended way ?

By the way, the necessary pre-requisite for doing this would be to have access 
to the “fast reference” operation:

     ML_Thms.thm_binding kind is_single thms txt 

which is at the moment not exported.
Again, what is the recommended way of doing this
(searching for a theorem in a local or global context) by its long name ?

[And please, don’t tell me it’s Eisbach.]


Best regards,

bu