doc-src/IsarRef/generic.tex
changeset 9847 32ce11c3f6b1
parent 9799 038b018f86f5
child 9905 14a71104a498
     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