On Sat, 1 Feb 2014, Makarius wrote:
If not, could one of the devs incorporate this tiny change please?
OK, I will try this out.
See now:
changeset: 55237:1e341728bae9
user:wenzelm
date:Sat Feb 01 20:46:19 2014 +0100
files: src/Tools/adhoc_overloading.ML
description:
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 resu
Reviving this old thread once more ;)
I think I need some clarifications first:
On 12/05/2013 05:05 PM, Florian Haftmann wrote:
Reviving this old thread, Peter and me found out what is actually going
on here.
Basically, nothing wrong. When abbreviations are declared, terms are
checked such th
On Sat, 1 Feb 2014, Makarius wrote:
Here is one more changeset to clarify that further: 04448228381d and its NEWS
entry:
* Proper context discipline for read_instantiate and instantiate_tac:
variables that are meant to become schematic need to be given as
fixed, and are generalized by the expl
On Sat, 1 Feb 2014, Peter Lammich wrote:
by (auto ... dest!: sym[of "pop A" for A] ...)
If this is now supported (it's not in 2013-2, where standard is already
deprecated): Nice feature! I have no objections left against removing
standard ;)
Here is one more changeset to clarify that f
Dear all,
recently I was working a lot with adhoc_overloading. Doing so I often
experienced that my output differed from my input (w.r.t. adhoc
overloading). At that time I did not think too much about it since being
able to input readable formulas was quite enough. But today I suddenly
had a
On Sat, 1 Feb 2014, Peter Lammich wrote:
So, ad-hoc massaging of a lemma is no longer possible?
E.g., I often use things like
by (auto ... dest!: sym[of "pop A", standard] ...)
in cases where I definitely do not want to expose the subgoal where the
"pop = ..." occurs into Isar.
So, if I got
So, ad-hoc massaging of a lemma is no longer possible?
E.g., I often use things like
by (auto ... dest!: sym[of "pop A", standard] ...)
in cases where I definitely do not want to expose the subgoal where the
"pop = ..." occurs into Isar.
So, if I got it right, the correct way would now be:
