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 Wed, 14 Aug 2013, Ondřej Kunčar wrote:
On 08/13/2013 04:19 PM, Andreas Lochbihler wrote:
Dear all,
in Isabelle abd760a19e22, I get the error Attempt to perform
non-trivial merge of theories when I include a bundle from another
theory and there are at least two imports.
In the attachment,
On Sat, 17 Aug 2013, Christian Sternagel wrote:
I propose to apply the following patch to the documentation of the function
package. (I found two tiny typos which could have been prevented by using
@{thm [source] ...} -- which might not have existed at the time of writing --
instead of @{text
