--- a/doc-src/Ref/ref.tex Sun Feb 05 21:00:38 2012 +0100 +++ b/doc-src/Ref/ref.tex Tue Feb 07 18:51:22 2012 +0100 @@ -49,7 +49,6 @@ \include{tactic} \include{thm} -\include{defining} \include{syntax} \include{substitution} \include{simplifier}