doc-src/IsarRef/generic.tex
changeset 9780 d25d6a977ea6
parent 9711 75df6a20b0b3
child 9799 038b018f86f5
     1.1 --- a/doc-src/IsarRef/generic.tex	Fri Sep 01 00:36:08 2000 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Fri Sep 01 00:48:12 2000 +0200
     1.3 @@ -699,18 +699,20 @@
     1.4  
     1.5  \subsection{Automated methods}\label{sec:classical-auto}
     1.6  
     1.7 -\indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{clarify}
     1.8 +\indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{best}
     1.9 +\indexisarmeth{safe}\indexisarmeth{clarify}
    1.10  \begin{matharray}{rcl}
    1.11 - blast & : & \isarmeth \\
    1.12 - fast & : & \isarmeth \\
    1.13 - best & : & \isarmeth \\
    1.14 - clarify & : & \isarmeth \\
    1.15 +  blast & : & \isarmeth \\
    1.16 +  fast & : & \isarmeth \\
    1.17 +  best & : & \isarmeth \\
    1.18 +  safe & : & \isarmeth \\
    1.19 +  clarify & : & \isarmeth \\
    1.20  \end{matharray}
    1.21  
    1.22  \begin{rail}
    1.23    'blast' ('!' ?) nat? (clamod * )
    1.24    ;
    1.25 -  ('fast' | 'best' | 'clarify') ('!' ?) (clamod * )
    1.26 +  ('fast' | 'best' | 'clarify' | 'safe') ('!' ?) (clamod * )
    1.27    ;
    1.28  
    1.29    clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
    1.30 @@ -724,9 +726,9 @@
    1.31    classical proof procedure in Isabelle that can handle actual object-logic
    1.32    rules as local assumptions ($fast$ etc.\ would just ignore non-atomic
    1.33    facts).
    1.34 -\item [$fast$, $best$, and $clarify$] refer to the generic classical reasoner.
    1.35 -  See \texttt{fast_tac}, \texttt{best_tac}, and \texttt{clarify_tac} in
    1.36 -  \cite[\S11]{isabelle-ref} for more information.
    1.37 +\item [$fast$, $best$, $safe$, and $clarify$] refer to the generic classical
    1.38 +  reasoner.  See \texttt{fast_tac}, \texttt{best_tac}, \texttt{safe_tac}, and
    1.39 +  \texttt{clarify_tac} in \cite[\S11]{isabelle-ref} for more information.
    1.40  \end{descr}
    1.41  
    1.42  Any of above methods support additional modifiers of the context of classical
    1.43 @@ -751,7 +753,9 @@
    1.44  \end{matharray}
    1.45  
    1.46  \begin{rail}
    1.47 -  ('auto' | 'force' | 'clarsimp' | 'fastsimp') ('!' ?) (clasimpmod * )
    1.48 +  'auto' '!'? (nat nat)? (clasimpmod * )
    1.49 +  ;
    1.50 +  ('force' | 'clarsimp' | 'fastsimp') '!'? (clasimpmod * )
    1.51    ;
    1.52  
    1.53    clasimpmod: ('simp' (() | 'add' | 'del' | 'only') |