Hi Florian,
Thank you for your suggestions. We will take them into account.
On 03/28/2012 07:26 AM, Florian Haftmann wrote:
http://isabelle.in.tum.de/reports/Isabelle/rev/861f53bd95fe#l1.53
the name given to the derived theorem is unsatisfactory. Since it is
not a »code-only« theorem, it
Yes, simps should not be used for special purpose rules.
Tobias
Am 28/03/2012 09:22, schrieb Lukas Bulwahn:
Hi Florian,
Thank you for your suggestions. We will take them into account.
On 03/28/2012 07:26 AM, Florian Haftmann wrote:
After a long discussion during a lunch break we decided to use
.rep_eq. I will also change _rsp to .rsp. What about _def?
Should I change it to .def as well? _def seems to be a
inconsistency, I guess because of historical reasons. Should new
packages use .def instead of _def?
Ondrej
On
On Wed, 28 Mar 2012, Ondřej Kunčar wrote:
After a long discussion during a lunch break we decided to use
.rep_eq. I will also change _rsp to .rsp. What about _def?
Should I change it to .def as well? _def seems to be a
inconsistency, I guess because of historical reasons. Should new
packages
This is explained by looking at the history: The typedef package
introduces names with underscores, quotient_type and quotient_def
inherit this from typedef.
This is a misunderstanding. The names generated by »typedef« have
always been retained »as they are«, merely for the sacrosanctity of
What I had in mind was something as can be found e.g. in
src/HOL/Library/Dlist.thy:
definition empty :: 'a dlist
where
empty = Dlist []
definition insert :: 'a \Rightarrow 'a dlist \Rightarrow 'a dlist
where
insert x dxs = Dlist (List.insert x (list_of_dlist dxs))
definition remove :: 'a
This is explained by looking at the history: The typedef package
introduces names with underscores, quotient_type and quotient_def
inherit this from typedef.
This is a misunderstanding. The names generated by »typedef« have
always been retained »as they are«, merely for the sacrosanctity
Hi Ondřej,
in
http://isabelle.in.tum.de/reports/Isabelle/rev/861f53bd95fe#l1.53
the name given to the derived theorem is unsatisfactory. Since it is
not a »code-only« theorem, it should not carry the »code« within. If it
would be a »code-only« theorem, the convention is to suffix with
