>> 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 sacrosa
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 \ 'a dlist \ 'a dlist"
where
"insert x dxs = Dlist (List.insert x (list_of_dlist dxs))"
definition remove :: "'a \ 'a dlist \ '
> 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
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 ne
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"?
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:
>> http://isabelle.in.tum.de/reports/Isabelle/re
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 shou
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
