# HG changeset patch
# User wenzelm
# Date 924108929 -7200
# Node ID 075f263a57bde278081e26d53df45862712ad7dd
# Parent  fd36b2e7d80ea0c12511e1ae9e462587991b1f14
remoced old set_current_thy;

diff -r fd36b2e7d80e -r 075f263a57bd doc-src/Logics/HOL.tex
--- a/doc-src/Logics/HOL.tex	Wed Apr 14 15:58:01 1999 +0200
+++ b/doc-src/Logics/HOL.tex	Wed Apr 14 18:55:29 1999 +0200
@@ -2971,9 +2971,8 @@
 {\out No subgoals!}
 \end{ttbox}
 If you run this example interactively, make sure your current theory contains
-theory \texttt{Set}, for example by executing
-\ttindex{set_current_thy}~{\tt"Set"}.  Otherwise the default claset may not
-contain the rules for set theory.
+theory \texttt{Set}, for example by executing \ttindex{context}~{\tt Set.thy}.
+Otherwise the default claset may not contain the rules for set theory.
 \index{higher-order logic|)}
 
 %%% Local Variables: 
diff -r fd36b2e7d80e -r 075f263a57bd doc-src/Logics/logics.ind
--- a/doc-src/Logics/logics.ind	Wed Apr 14 15:58:01 1999 +0200
+++ b/doc-src/Logics/logics.ind	Wed Apr 14 18:55:29 1999 +0200
@@ -60,6 +60,7 @@
   \item {\tt and_def} theorem, 10
   \item {\tt arg_cong} theorem, 11
   \item {\tt Arith} theory, 26, 82
+  \item {\tt arith_tac}, 27
   \item assumptions
     \subitem in {\CTT}, 71, 81
 
@@ -116,6 +117,7 @@
   \item {\tt conL} theorem, 62
   \item {\tt conR} theorem, 62
   \item Constructive Type Theory, 71--93
+  \item {\tt context}, 57
   \item {\tt contr} constant, 72
   \item {\tt could_res}, \bold{64}
   \item {\tt could_resolve_seq}, \bold{64}
@@ -499,7 +501,6 @@
   \item {\tt Set} theory, 13, 16
   \item {\tt set} constant, 28
   \item {\tt set} type, 13
-  \item {\tt set_current_thy}, 57
   \item {\tt set_diff_def} theorem, 17
   \item {\tt show_sorts}, 8
   \item {\tt show_types}, 8
@@ -595,7 +596,6 @@
   \item {\tt trans} theorem, 11, 61
   \item {\tt trans_elem} theorem, 75
   \item {\tt trans_red} theorem, 75
-  \item {\tt trans_tac}, 27
   \item {\tt trans_type} theorem, 75
   \item {\tt True} constant, 6, 59
   \item {\tt True_def} theorem, 10, 61