This is a tricky point, but on balance, I think it's better to have complete
documentation even if it draws people's attention to things they should
overlook.
Larry
On 19 Aug 2013, at 22:41, Makarius makar...@sketis.net wrote:
Of course you are welcome to update your documentation snippet
Am 17/08/2013 15:20, schrieb Makarius:
On Thu, 15 Aug 2013, Lawrence Paulson wrote:
I think that the only way to achieve the documented behaviour is to replace
all schematic variables in the goal by Frees before attempting resolution.
Which can be done safely outside the kernel.
If you
Your point of view makes sense on general principles, but not in this
particular case.
I had actually forgotten that these tactics existed. But they form a core part
of the classical reasoner, and there are good reasons why they work the way
they do. The proof state could be very large, so
Am 19/08/2013 12:45, schrieb Lawrence Paulson:
Your point of view makes sense on general principles, but not in this
particular case.
I had actually forgotten that these tactics existed. But they form a core
part of the classical reasoner, and there are good reasons why they work the
way
I was about to change the documentation to say just that, only to discover that
almost exactly the same change was made in November 2008.
wenzelm 50072 Wed Nov 07 16:02:43 2012 +0100
src/Doc/IsarImplementation/Tactic.thy:321: \item @{ML match_tac}, @{ML
ematch_tac}, @{ML dmatch_tac}, and
On Sun, 18 Aug 2013, Lars Noschinski wrote:
Combinators like Subgoal.FOCUS have replaced a lot of old-style
tinkering with goals; within the focused parts things are fixed and
don't get instantiated by accident.
I seem to remember a discussion on the mailing list that Subgoal.FOCUS
does not
On Mon, 19 Aug 2013, Tobias Nipkow wrote:
Am 17/08/2013 15:20, schrieb Makarius:
On Thu, 15 Aug 2013, Lawrence Paulson wrote:
I think that the only way to achieve the documented behaviour is to replace
all schematic variables in the goal by Frees before attempting resolution.
Which can be
On Mon, 19 Aug 2013, Lawrence Paulson wrote:
I was about to change the documentation to say just that, only to
discover that almost exactly the same change was made in November 2008.
wenzelm 50072 Wed Nov 07 16:02:43 2012 +0100
src/Doc/IsarImplementation/Tactic.thy:321: \item @{ML
On Thu, 15 Aug 2013, Lawrence Paulson wrote:
I think that the only way to achieve the documented behaviour is to
replace all schematic variables in the goal by Frees before attempting
resolution.
If you would do that for the quais-match mode of unify.ML in general it
would probably break
On Thu, 15 Aug 2013, Lawrence Paulson wrote:
On 13 Aug 2013, at 10:35, Lars Noschinski nosch...@in.tum.de wrote:
It might be interesting to note that also Unify.matchers is not able to
match such term.
This old thread on Unify.matchers might be also interesting:
Probably you are right.
Larry
On 17 Aug 2013, at 14:20, Makarius makar...@sketis.net wrote:
On Thu, 15 Aug 2013, Lawrence Paulson wrote:
I think that the only way to achieve the documented behaviour is to replace
all schematic variables in the goal by Frees before attempting resolution.
I think that the only way to achieve the documented behaviour is to replace all
schematic variables in the goal by Frees before attempting resolution. I'm not
sure what effect this would have on performance.
Larry
On 13 Aug 2013, at 10:35, Lars Noschinski nosch...@in.tum.de wrote:
On
12 matches
Mail list logo
