# HG changeset patch
# User wenzelm
# Date 903978733 -7200
# Node ID e27558a68b8d8c0f661c1e4d03d75850d366d305
# Parent  ba0470fe09fcf1fa45e162bb5f40e0b95014b64a
emacs local vars;

diff -r ba0470fe09fc -r e27558a68b8d doc-src/Ref/classical.tex
--- 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: 
diff -r ba0470fe09fc -r e27558a68b8d doc-src/Ref/defining.tex
--- 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: 
diff -r ba0470fe09fc -r e27558a68b8d doc-src/Ref/goals.tex
--- 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: 
diff -r ba0470fe09fc -r e27558a68b8d doc-src/Ref/introduction.tex
--- 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: 
diff -r ba0470fe09fc -r e27558a68b8d doc-src/Ref/substitution.tex
--- 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: 
diff -r ba0470fe09fc -r e27558a68b8d doc-src/Ref/syntax.tex
--- 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: 
diff -r ba0470fe09fc -r e27558a68b8d doc-src/Ref/tactic.tex
--- 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: 
diff -r ba0470fe09fc -r e27558a68b8d doc-src/Ref/tctical.tex
--- 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: 
diff -r ba0470fe09fc -r e27558a68b8d doc-src/Ref/thm.tex
--- 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: