<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 Chris,<br>
<br>
I've pushed it to the testboard (and will push it to the
repository in case of success):<br>
<br>
<a 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 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 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>