added 'iff' modifier;
authorwenzelm
Tue Sep 05 18:43:54 2000 +0200 (2000-09-05)
changeset 984732ce11c3f6b1
parent 9846 bb848beb53f6
child 9848 afc54ca6dc6f
added 'iff' modifier;
removed 'other' modifier;
doc-src/IsarRef/generic.tex
     1.1 --- a/doc-src/IsarRef/generic.tex	Tue Sep 05 18:43:22 2000 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Tue Sep 05 18:43:54 2000 +0200
     1.3 @@ -528,7 +528,7 @@
     1.4    opt: '(' (noasm | noasmsimp | noasmuse) ')'
     1.5    ;
     1.6    simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
     1.7 -    'split' (() | 'add' | 'del') | 'other') ':' thmrefs
     1.8 +    'split' (() | 'add' | 'del')) ':' thmrefs
     1.9    ;
    1.10  \end{rail}
    1.11  
    1.12 @@ -545,10 +545,6 @@
    1.13    Splitter (see also \cite{isabelle-ref}), the default is to add.  This works
    1.14    only if the Simplifier method has been properly setup to include the
    1.15    Splitter (all major object logics such HOL, HOLCF, FOL, ZF do this already).
    1.16 -  
    1.17 -  \medskip The \railtterm{other} modifier ignores its arguments.
    1.18 -  Nevertheless, additional kinds of rules may be declared by including
    1.19 -  appropriate attributes in the specification.
    1.20  \item [$simp_all$] is similar to $simp$, but acts on all goals.
    1.21  \end{descr}
    1.22  
    1.23 @@ -659,7 +655,7 @@
    1.24  \end{descr}
    1.25  
    1.26  
    1.27 -\section{The Classical Reasoner}
    1.28 +\section{The Classical Reasoner}\label{sec:classical}
    1.29  
    1.30  \subsection{Basic methods}\label{sec:classical-basic}
    1.31  
    1.32 @@ -746,7 +742,7 @@
    1.33  \S\ref{sec:simp}).
    1.34  
    1.35  
    1.36 -\subsection{Combined automated methods}
    1.37 +\subsection{Combined automated methods}\label{sec:clasimp}
    1.38  
    1.39  \indexisarmeth{auto}\indexisarmeth{force}\indexisarmeth{clarsimp}
    1.40  \indexisarmeth{fastsimp}\indexisarmeth{slowsimp}\indexisarmeth{bestsimp}
    1.41 @@ -766,7 +762,7 @@
    1.42    ;
    1.43  
    1.44    clasimpmod: ('simp' (() | 'add' | 'del' | 'only') |
    1.45 -    'cong' (() | 'add' | 'del') | ('split' (() | 'add' | 'del')) | 'other' |
    1.46 +    ('cong' | 'split' | 'iff') (() | 'add' | 'del') |
    1.47      (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs
    1.48  \end{rail}
    1.49