doc-src/IsarRef/generic.tex

--- a/doc-src/IsarRef/generic.tex	Tue Sep 05 18:43:22 2000 +0200
+++ b/doc-src/IsarRef/generic.tex	Tue Sep 05 18:43:54 2000 +0200
@@ -528,7 +528,7 @@
   opt: '(' (noasm | noasmsimp | noasmuse) ')'
   ;
   simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
-    'split' (() | 'add' | 'del') | 'other') ':' thmrefs
+    'split' (() | 'add' | 'del')) ':' thmrefs
   ;
 \end{rail}
 
@@ -545,10 +545,6 @@
   Splitter (see also \cite{isabelle-ref}), the default is to add.  This works
   only if the Simplifier method has been properly setup to include the
   Splitter (all major object logics such HOL, HOLCF, FOL, ZF do this already).
-  
-  \medskip The \railtterm{other} modifier ignores its arguments.
-  Nevertheless, additional kinds of rules may be declared by including
-  appropriate attributes in the specification.
 \item [$simp_all$] is similar to $simp$, but acts on all goals.
 \end{descr}
 
@@ -659,7 +655,7 @@
 \end{descr}
 
 
-\section{The Classical Reasoner}
+\section{The Classical Reasoner}\label{sec:classical}
 
 \subsection{Basic methods}\label{sec:classical-basic}
 
@@ -746,7 +742,7 @@
 \S\ref{sec:simp}).
 
 
-\subsection{Combined automated methods}
+\subsection{Combined automated methods}\label{sec:clasimp}
 
 \indexisarmeth{auto}\indexisarmeth{force}\indexisarmeth{clarsimp}
 \indexisarmeth{fastsimp}\indexisarmeth{slowsimp}\indexisarmeth{bestsimp}
@@ -766,7 +762,7 @@
   ;
 
   clasimpmod: ('simp' (() | 'add' | 'del' | 'only') |
-    'cong' (() | 'add' | 'del') | ('split' (() | 'add' | 'del')) | 'other' |
+    ('cong' | 'split' | 'iff') (() | 'add' | 'del') |
     (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs
 \end{rail}