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

[Makarius]

On 21/06/16 11:40, Burkhart Wolff wrote:

> 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.

Record.get_info did not change in Isabelle2016. What do you mean precisely?

The old datatype package has been superseded by BNF datatypes about 2
years ago. The BNF guys can say how to access the datatype info,
although that has changed significantly.

I somehow suspect that you are trying to move from a very old Isabelle
version to Isabelle2016, but this is a bad idea. You should always
follow each Isabelle release step by step.


> 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 ?

I don't understand that paragraph. How is this related?


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

How is this related at all?


	Makarius