# HG changeset patch
# User wenzelm
# Date 891693019 -7200
# Node ID 7cfc85fc6fd701164e44ea23f947e030c51ee272
# Parent  d66477d29598c93b6f7600d1611ddf64bf3269d2
no open Simplifier;

diff -r d66477d29598 -r 7cfc85fc6fd7 doc-src/Ref/simplifier.tex
--- a/doc-src/Ref/simplifier.tex	Sat Apr 04 14:27:11 1998 +0200
+++ b/doc-src/Ref/simplifier.tex	Sat Apr 04 14:30:19 1998 +0200
@@ -1308,14 +1308,11 @@
 
 \subsection{Making the initial simpset}
 
-It is time to assemble these items.  We open module \texttt{Simplifier}
-to gain direct access to its components.  We define the infix operator
+It is time to assemble these items.  We define the infix operator
 \ttindex{addcongs} to insert congruence rules; given a list of
 theorems, it converts their conclusions into meta-equalities and
 passes them to \ttindex{addeqcongs}.
 \begin{ttbox}
-open Simplifier;
-\ttbreak
 infix 4 addcongs;
 fun ss addcongs congs =
     ss addeqcongs (congs RL [eq_reflection,iff_reflection]);