Re: [isabelle-dev] AFP/Lifting_Definition_Option

The first step would be to contact the authors of the entry. If they agree that it is superseded by something else, the entry can be made empty, with an explanation/referral to whatever replaced it. Cheers, Gerwin > On 06.10.2015, at 03:15, Makarius wrote: > > What is the

Re: [isabelle-dev] Exposing some functions of the API

Hi, During some programming tasks, I had to use the following functions: BNF_FP_Def_Sugar.co_datatype_cmd note that these *_cmd functions are merely supposed to be used when declaring Isar commands; dervived Isabelle/ML code is always supposed to work with proper internalized entities (types

Re: [isabelle-dev] Exposing some functions of the API

On Thu, 1 Oct 2015, Florian Haftmann wrote: Classical.rule_tac Is Method.rule_tac sufficient for you purpose? It is more elementary (and thus more predictable). I have exported this morally public function in Isabelle/0a4c364df431. But the purpose of all that was not explained so far.