minor corrections
Fri, 01 May 1998 22:40:20 +0200
changeset 4885 54fa88124d52
parent 4884 1ec740e30811
child 4886 31f23b8d6851
minor corrections
--- a/doc-src/Ref/classical.tex	Fri May 01 22:30:42 1998 +0200
+++ b/doc-src/Ref/classical.tex	Fri May 01 22:40:20 1998 +0200
@@ -399,14 +399,15 @@
 \index{simplification!from classical reasoner} The wrapper tacticals
 underly the operators addss and addSss, which are used as primitives 
-for the automatic tactics described in \S\label{sec:automatic-tactics}.
+for the automatic tactics described in \S\ref{sec:automatic-tactics}.
 Strictly speaking, both operators are not part of the classical reasoner. 
 They should be defined when the simplifier is installed:
 infix 4 addSss addss;
 fun  cs addSss ss = cs addSaltern ("safe_asm_full_simp_tac",
                          CHANGED o (safe_asm_full_simp_tac ss));
-fun  cs addss  ss = cs addbefore  ("asm_full_simp_tac", asm_full_simp_tac ss);
+fun  cs addss  ss = cs addbefore  ("asm_full_simp_tac", 
+                                    asm_full_simp_tac ss);
 Being defined as wrappers, these operators are inappropriate for adding more 
@@ -499,7 +500,7 @@
 The automatic tactics attempt to prove goals using a combination of
 simplification and classical reasoning. 
 \item[\ttindexbold{auto_tac $(cs,ss)$}] is intended for situations where 
 there are a lot of mostly trivial subgoals; it proves all the easy ones, 
 leaving the ones it cannot prove.
@@ -507,18 +508,13 @@
 \item[\ttindexbold{force_tac} $(cs,ss)$ $i$] is intended to prove subgoal~$i$ 
 completely. It tries to apply all fancy tactics it knows about, 
 performing a rather exhaustive search.
 They must be supplied both a simpset and a claset; therefore 
 they are most easily called as \texttt{Auto_tac} and \texttt{Force_tac}, which 
 use the default claset and simpset (see \S\ref{sec:current-claset} below). 
-For interactive use, the shorthand \texttt{auto();} abbreviates 
-by Auto_tac;
-while \texttt{force 1;} abbreviates 
-by (Force_tac 1);
+For interactive use, 
+the shorthand \texttt{auto();} abbreviates \texttt{by Auto_tac;} 
+while \texttt{force 1;} abbreviates \texttt{by (Force_tac 1);}
 \subsection{Other classical tactics}