--- a/doc-src/Ref/classical.tex Mon Aug 24 19:11:13 1998 +0200
+++ b/doc-src/Ref/classical.tex Mon Aug 24 19:12:13 1998 +0200
@@ -755,3 +755,9 @@
Provers/classical.ML} in the Isabelle sources.
\index{classical reasoner|)}
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "ref"
+%%% End:
--- a/doc-src/Ref/defining.tex Mon Aug 24 19:11:13 1998 +0200
+++ b/doc-src/Ref/defining.tex Mon Aug 24 19:12:13 1998 +0200
@@ -886,3 +886,9 @@
by (eresolve_tac [MinIF.FalseE] 1);
\end{ttbox}
Try this as an exercise!
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "ref"
+%%% End:
--- a/doc-src/Ref/goals.tex Mon Aug 24 19:11:13 1998 +0200
+++ b/doc-src/Ref/goals.tex Mon Aug 24 19:12:13 1998 +0200
@@ -590,3 +590,9 @@
\index{subgoal module|)}
\index{proofs|)}
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "ref"
+%%% End:
--- a/doc-src/Ref/introduction.tex Mon Aug 24 19:11:13 1998 +0200
+++ b/doc-src/Ref/introduction.tex Mon Aug 24 19:12:13 1998 +0200
@@ -321,3 +321,9 @@
\end{warn}
\index{sessions|)}
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "ref"
+%%% End:
--- a/doc-src/Ref/substitution.tex Mon Aug 24 19:11:13 1998 +0200
+++ b/doc-src/Ref/substitution.tex Mon Aug 24 19:12:13 1998 +0200
@@ -206,3 +206,9 @@
by calling \hbox{\tt resolve_tac\ts[imp_intr]}.
\index{equality|)}\index{tactics!substitution|)}
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "ref"
+%%% End:
--- a/doc-src/Ref/syntax.tex Mon Aug 24 19:11:13 1998 +0200
+++ b/doc-src/Ref/syntax.tex Mon Aug 24 19:12:13 1998 +0200
@@ -901,3 +901,9 @@
%FIXME example (?)
\index{token translations|)}
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "ref"
+%%% End:
--- a/doc-src/Ref/tactic.tex Mon Aug 24 19:11:13 1998 +0200
+++ b/doc-src/Ref/tactic.tex Mon Aug 24 19:12:13 1998 +0200
@@ -703,3 +703,9 @@
\end{ttdescription}
\index{tactics|)}
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "ref"
+%%% End:
--- a/doc-src/Ref/tctical.tex Mon Aug 24 19:11:13 1998 +0200
+++ b/doc-src/Ref/tctical.tex Mon Aug 24 19:12:13 1998 +0200
@@ -509,3 +509,9 @@
\end{center}
\index{tacticals|)}
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "ref"
+%%% End:
--- a/doc-src/Ref/thm.tex Mon Aug 24 19:11:13 1998 +0200
+++ b/doc-src/Ref/thm.tex Mon Aug 24 19:12:13 1998 +0200
@@ -817,3 +817,9 @@
\index{proof objects|)}
\index{theorems|)}
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "ref"
+%%% End: