[isabelle-dev] [isabelle] match_tac, schematic and bound variables

[Lawrence Paulson]

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 <makarius at sketis.net> wrote:

> 
> 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.