[isabelle-dev] Acces to internal interfaces ...
Burkhart.Wolff at lri.fr
Tue Jun 21 11:40:53 CEST 2016
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.]
More information about the isabelle-dev