On Sat, 1 Feb 2014, Christian Sternagel wrote:
So my idea was to instead use top-down rewriting (i.e., first replace
maximal subterms that fit a given pattern). This is what
"Pattern.rewrite_term_top" does, right? So after replacing
"rewrite_term" by "rewrite_term_top", I get the expected results.
Now my question. Can anybody think of a reason why "rewrite_term_top"
would not be generally preferable over "rewrite_term" inside of
"insert_overloaded"?
This is an old story. Printing usually works better top-down, e.g. see
good old 'translations' with their yo-yo strategy. When 'abbreviation'
was introduced, there was Pattern.rewrite_term, but not
Pattern.rewrite_term_top yet, so there was no other way.
I kept telling Stefan Berghofer about that omission until he made an
laternative version in 2010: see 6e45e4c94751, 5d2fe4e09354 (with typical
tell-nothing log entries).
So in analogy, the same will probably work for adhoc_overloading as well,
without going through all the reasoning again.
If not, could one of the devs incorporate this tiny change please?
OK, I will try this out.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
