[isabelle-dev] [isabelle] match_tac, schematic and bound variables
lp15 at cam.ac.uk
Tue Aug 20 11:22:40 CEST 2013
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.
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.
More information about the isabelle-dev