doc-src/IsarRef/generic.tex
changeset 7981 5120a2a15d06
parent 7974 34245feb6e82
child 7987 d9aef93c0e32
     1.1 --- a/doc-src/IsarRef/generic.tex	Sat Oct 30 20:12:23 1999 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Sat Oct 30 20:13:16 1999 +0200
     1.3 @@ -353,7 +353,7 @@
     1.4  \end{descr}
     1.5  
     1.6  
     1.7 -\subsection{Automatic methods}\label{sec:classical-auto}
     1.8 +\subsection{Automated methods}\label{sec:classical-auto}
     1.9  
    1.10  \indexisarmeth{blast}
    1.11  \indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{slow}\indexisarmeth{slow-best}
    1.12 @@ -391,7 +391,7 @@
    1.13  \S\ref{sec:classical-mod}.
    1.14  
    1.15  
    1.16 -\subsection{Combined automatic methods}
    1.17 +\subsection{Combined automated methods}
    1.18  
    1.19  \indexisarmeth{auto}\indexisarmeth{force}
    1.20  \begin{matharray}{rcl}
    1.21 @@ -437,7 +437,7 @@
    1.22  \item [$intro$, $elim$, $dest$] add introduction, elimination, destruct rules,
    1.23    respectively.  By default, rules are considered as \emph{safe}, while a
    1.24    single ``!'' classifies as \emph{unsafe}, and ``!!'' as \emph{extra} (i.e.\ 
    1.25 -  not applied in the search-oriented automatic methods, but only $rule$).
    1.26 +  not applied in the search-oriented automated methods, but only $rule$).
    1.27    
    1.28  \item [$iff$] declares equations both as rewrite rules for the simplifier and
    1.29    classical reasoning rules.