# HG changeset patch
# User wenzelm
# Date 1210242690 -7200
# Node ID d889d57445dcff95156e4406290a55ba47fd5045
# Parent  df50bc1249d72e3b0f20f8a17e035127b4fda5a5
unused;

diff -r df50bc1249d7 -r d889d57445dc doc-src/IsarRef/Thy/document/session.tex
--- a/doc-src/IsarRef/Thy/document/session.tex	Thu May 08 12:29:18 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-\input{intro.tex}
-
-\input{syntax.tex}
-
-\input{pure.tex}
-
-\input{Generic.tex}
-
-\input{HOL_Specific.tex}
-
-\input{Quick_Reference.tex}
-
-\input{ML_Tactic.tex}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: