<html>
<head>
<meta content="text/html; charset=UTF-8" http-equiv="Content-Type">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<div class="moz-cite-prefix">Hi,<br>
<br>
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:<br>
<br>
consts T :: 'a<br>
adhoc_overloading T True<br>
declare[[show_variants = false]]<br>
term T<br>
<br>
The term command will show True (=the expected output with
show_variants = true), whereas T is expected with show_variants =
false.<br>
<br>
Cheers,<br>
Dmitriy<br>
<br>
On 28.01.2015 10:40, Dmitriy Traytel wrote:<br>
</div>
<blockquote cite="mid:54C8AE73.7010203@in.tum.de" type="cite">
<meta content="text/html; charset=UTF-8" http-equiv="Content-Type">
<div class="moz-cite-prefix">Hi Chris,<br>
<br>
I've pushed it to the testboard (and will push it to the
repository in case of success):<br>
<br>
<a moz-do-not-send="true" class="moz-txt-link-freetext"
href="http://isabelle.in.tum.de/testboard/Isabelle/rev/0d7de4d99eac">http://isabelle.in.tum.de/testboard/Isabelle/rev/0d7de4d99eac</a><br>
<br>
Cheers,<br>
Dmitriy<br>
<br>
On 28.01.2015 09:55, Christian Sternagel wrote:<br>
</div>
<blockquote cite="mid:54C8A40B.4030508@gmail.com" type="cite">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. <br>
<br>
By peeking into the sources - even without understanding much of
it ;) - it can be seen that the flag "abbrev_mode" is checked
for abbreviations. By doing the same inside "adhoc_overloading"
the ugly output I presented earlier, turned into beautiful
symbols. <br>
<br>
Could one of the developers be so kind to apply the attached
(mq) patch (after testing it of course) ;) ? <br>
<br>
cheers <br>
<br>
chris <br>
<br>
On 01/16/2015 02:40 PM, Christian Sternagel wrote: <br>
<blockquote type="cite">Here is a related thread <br>
<br>
<br>
<a moz-do-not-send="true" class="moz-txt-link-freetext"
href="https://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04950.html">https://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04950.html</a>
<br>
<br>
<br>
which was originated by myself ;) (how embarassing). <br>
<br>
cheers <br>
<br>
chris <br>
<br>
On 01/16/2015 02:35 PM, Christian Sternagel wrote: <br>
<blockquote type="cite">Dear all, <br>
<br>
in Isabelle2014 as well as c7f6f01ede15 I noticed that the
output when <br>
using adhoc overloading together with abbreviations is not
optimal <br>
(maybe this was already discovered before but I forgot about
it). Now, <br>
it turns out that the same issue (at least superficially
it's the same, <br>
but maybe caused by different reasons) arises also for
definitions in <br>
local theory contexts (or are those the same as mere
abbreviations?). <br>
<br>
Let me illustrate what I'm talking about by the following
example: <br>
<br>
theory Foo <br>
imports <br>
Main <br>
"~~/src/Tools/Adhoc_Overloading" <br>
begin <br>
<br>
consts SHARP :: "'a ⇒ 'b" ("♯") <br>
<br>
context <br>
fixes shp :: "'a ⇒ 'a" <br>
begin <br>
<br>
adhoc_overloading <br>
SHARP shp <br>
<br>
definition le_sharp (infix "≤⇩♯" 50) <br>
where <br>
"xs ≤⇩♯ ys ≡ list_all2 (λx y. y = x ∨ y = ♯ x) xs ys" <br>
<br>
term "xs ≤⇩♯ ys" <br>
text ‹ <br>
Result in @{term "Foo.le_sharp ♯ xs ys"} instead of <br>
more desirable @{term "xs ≤⇩♯ ys"}. (The same happens <br>
when we turn the above definition into an abbreviation.)
<br>
› <br>
<br>
end <br>
<br>
text ‹ <br>
In the "global" theory this also happens, but only for <br>
abbreviations, not for definitions. <br>
› <br>
<br>
definition "shp = id" <br>
<br>
adhoc_overloading SHARP shp <br>
<br>
definition le_sharp' (infix "≤⇩♯" 50) <br>
where <br>
"xs ≤⇩♯ ys ≡ list_all2 (λx y. y = x ∨ y = ♯ x) xs ys" <br>
<br>
term "xs ≤⇩♯ ys" <br>
<br>
end <br>
<br>
Unfortunately, at the moment I do not have time to look into
adhoc <br>
overloading myself, but let this thread be a reminder. If
anybody else <br>
can provide explanations/comments/solutions, please go
ahead! <br>
<br>
cheers <br>
<br>
chris <br>
</blockquote>
</blockquote>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
isabelle-dev mailing list
<a moz-do-not-send="true" class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a moz-do-not-send="true" class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
<br>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>