diff -r 6c8cd101f875 -r eb15fd4cd1ad doc-src/IsarRef/Thy/document/session.tex
--- a/doc-src/IsarRef/Thy/document/session.tex	Tue Apr 22 22:00:31 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/session.tex	Wed Apr 23 12:13:08 2008 +0200
@@ -1,3 +1,5 @@
+\input{intro.tex}
+
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"