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 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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
