# HG changeset patch
# User wenzelm
# Date 968172234 -7200
# Node ID 32ce11c3f6b1e56142f713b0c6f4ffb372265cc7
# Parent  bb848beb53f6c463e440550a4d5a09101364fde5
added 'iff' modifier;
removed 'other' modifier;

diff -r bb848beb53f6 -r 32ce11c3f6b1 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}