On Tue, 6 Oct 2015, Frédéric Tuong wrote:
Whereas AFP/Isabelle_Meta_Model correctly compiles with Isabelle 2015, I
plan to submit an updated version of the overall so that it will also
compile with the Isabelle development version.
You should also try to eliminate all these clones of Isabelle
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 t
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.
It
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
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 enti
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 le
