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 match_tac}, @{ML
ematch_tac}, @{ML dmatch_tac}, and @{ML
wenzelm 50072 Wed Nov 07 16:02:43 2012 +0100
src/Doc/IsarImplementation/Tactic.thy:322: bimatch_tac} are similar to @{ML
resolve_tac}, @{ML eresolve_tac},
wenzelm 50072 Wed Nov 07 16:02:43 2012 +0100
src/Doc/IsarImplementation/Tactic.thy:323: @{ML dresolve_tac}, and @{ML
biresolve_tac}, respectively, but do
wenzelm 50072 Wed Nov 07 16:02:43 2012 +0100
src/Doc/IsarImplementation/Tactic.thy:324: not instantiate schematic
variables in the goal state.
wenzelm 28783 Thu Nov 13 22:05:49 2008 +0100
doc-src/IsarImplementation/Thy/tactic.thy:321:
wenzelm 28783 Thu Nov 13 22:05:49 2008 +0100
doc-src/IsarImplementation/Thy/tactic.thy:322: Flexible subgoals are not
updated at will, but are left alone.
wenzelm 28783 Thu Nov 13 22:05:49 2008 +0100
doc-src/IsarImplementation/Thy/tactic.thy:323: Strictly speaking, matching
means to treat the unknowns in the goal
wenzelm 28783 Thu Nov 13 22:05:49 2008 +0100
doc-src/IsarImplementation/Thy/tactic.thy:324: state as constants; these
tactics merely discard unifiers that would
wenzelm 28783 Thu Nov 13 22:05:49 2008 +0100
doc-src/IsarImplementation/Thy/tactic.thy:325: update the goal state.
I cannot read the above copy paste from what you see on your screen. When
pointing to the history you need to tell the changeset id (abbreviated
hashkey) not the phyical index or date.
Refurbishing all these old manuals over several years, I have moved around
things between different files and directories, so that match_tac is now
in the "implementation" manual here:
http://isabelle.in.tum.de/repos/isabelle/file/15fe0ca088b3/src/Doc/IsarImplementation/Tactic.thy#l336
It originally comes from your initial version of the "ref" manual
http://isabelle.in.tum.de/repos/isabelle/annotate/d8205bb279a7/doc-src/Ref/tactic.tex#l74
This text from Nov 1993 gives a sense of the anciety of this stuff.
Clearly the system around it has improved way beyond the "research
prototype" nature of the original "Isabelle" with unify.ML at its core.
(I am still convinced that it was a very good approach, and don't want to
see it destroyed at the very core.)
Of course you are welcome to update your documentation snippet on
match_tac. I am also ready to remove it from the documentation
altogether. Brushing up the old "ref" material since 2008 for the
"implementation" manual has introduced some bias towards vintage
operations. E.g. some readers have pointed out the relative insignificance
of the res_inst_tac family just after I had reconstructed that section --
and they were right about it.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
