Hi Christian,
> Thanks for pointing this out. While yours is a valid observation, it
> seems that observing "abbrev_mode" is not enough to obtain nicer output,
> i.e., when using
>
> fun uncheck ctxt ts =
> - if Config.get ctxt show_variants orelse exists (is_none o try
> Term.type_of) ts then
On 01/28/2015 06:15 PM, Florian Haftmann wrote:
fun uncheck ctxt ts =
- if Config.get ctxt show_variants orelse exists (is_none o try Term.type_of)
ts then ts
+ if Proof_Context.abbrev_mode ctxt orelse
+Config.get ctxt show_variants orelse
+exists (can Term.type_of) ts then ts
> fun uncheck ctxt ts =
> - if Config.get ctxt show_variants orelse exists (is_none o try
> Term.type_of) ts then ts
> + if Proof_Context.abbrev_mode ctxt orelse
> +Config.get ctxt show_variants orelse
> +exists (can Term.type_of) ts then ts
>else map (insert_overloaded ctxt) ts;
N
Oops! You are right, of course. I was so delighted to see the nice
output for my example that I completely forgot about checking whether
previously "correct" results of adhoc overloading are still okay.
Thanks for testing and your report! I will have to investigate further ...
cheers
chris
O
Hi,
after looking a little bit closer at the proposed patch, I doubt that it
has the desired effect: it basically disables the uncheck phase almost
always (e.g. for term and lemma). Consider:
consts T :: 'a
adhoc_overloading T True
declare[[show_variants = false]]
term T
The term command wil
Hi Chris,
I've pushed it to the testboard (and will push it to the repository in
case of success):
http://isabelle.in.tum.de/testboard/Isabelle/rev/0d7de4d99eac
Cheers,
Dmitriy
On 28.01.2015 09:55, Christian Sternagel wrote:
It is amazing how easy some things get when a wizard is looking ove
It is amazing how easy some things get when a wizard is looking over
your shoulder (thanks Florian!). It turns out that adhoc overloading
(which is in essence very similar to abbreviations) did not observe some
conventions that are followed by the "abbreviation" command.
By peeking into the so
Here is a related thread
https://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04950.html
which was originated by myself ;) (how embarassing).
cheers
chris
On 01/16/2015 02:35 PM, Christian Sternagel wrote:
Dear all,
in Isabelle2014 as well as c7f6f01ede15 I notic
Dear all,
in Isabelle2014 as well as c7f6f01ede15 I noticed that the output when
using adhoc overloading together with abbreviations is not optimal
(maybe this was already discovered before but I forgot about it). Now,
it turns out that the same issue (at least superficially it's the same,
bu
