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
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.
Hi Frédéric,
> 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
Hi Florian, Frédéric,
Sorry for not answering this earlier. Somehow, I failed to notice that two of
the three functions are my responsibility.
>> During some programming tasks, I had to use the following functions:
>>
>> BNF_FP_Def_Sugar.co_datatype_cmd
>
> note that these *_cmd functions are
Dear all,
During some programming tasks, I had to use the following functions:
BNF_FP_Def_Sugar.co_datatype_cmd
Classical.rule_tac
Metis_Tactic.metis_method
However they only appear inside their respective structures, would it be
possible to write their corresponding types in signatures, at
