diff -r 287182c2f23a -r e68c3861b8db doc-src/Ref/ref.tex
--- a/doc-src/Ref/ref.tex	Mon Jun 06 19:08:46 2011 +0200
+++ b/doc-src/Ref/ref.tex	Mon Jun 06 19:13:48 2011 +0200
@@ -47,7 +47,6 @@
 
 \pagenumbering{roman} \tableofcontents \clearfirst
 
-\include{introduction}
 \include{tactic}
 \include{tctical}
 \include{thm}