doc-src/IsarRef/generic.tex
changeset 9408 d3d56e1d2ec1
parent 9232 96722b04f2ae
child 9438 6131037f8a11
     1.1 --- a/doc-src/IsarRef/generic.tex	Sun Jul 23 11:59:21 2000 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Sun Jul 23 12:01:05 2000 +0200
     1.3 @@ -550,7 +550,7 @@
     1.4    ('fast' | 'best' | 'slow' | slowbest) ('!' ?) (clamod * )
     1.5    ;
     1.6  
     1.7 -  clamod: (('intro' | 'elim' | 'dest') (() | '?' | '??') | 'del') ':' thmrefs
     1.8 +  clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
     1.9    ;
    1.10  \end{rail}
    1.11  
    1.12 @@ -586,7 +586,7 @@
    1.13  
    1.14    clasimpmod: ('simp' (() | 'add' | 'del' | 'only') | 'other' |
    1.15      ('split' (() | 'add' | 'del')) |
    1.16 -    (('intro' | 'elim' | 'dest') (() | '?' | '??') | 'del')) ':' thmrefs
    1.17 +    (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs
    1.18  \end{rail}
    1.19  
    1.20  \begin{descr}
    1.21 @@ -618,7 +618,7 @@
    1.22  \end{matharray}
    1.23  
    1.24  \begin{rail}
    1.25 -  ('intro' | 'elim' | 'dest') (() | '?' | '??')
    1.26 +  ('intro' | 'elim' | 'dest') ('!' | () | '?')
    1.27    ;
    1.28    'iff' (() | 'add' | 'del')
    1.29  \end{rail}
    1.30 @@ -629,9 +629,10 @@
    1.31    \cite{isabelle-ref}.  This is a diagnostic command; $undo$ does not apply.
    1.32  \item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
    1.33    destruct rules, respectively.  By default, rules are considered as
    1.34 -  \emph{safe}, while a single ``?'' classifies as \emph{unsafe}, and ``??'' as
    1.35 -  \emph{extra} (i.e.\ not applied in the search-oriented automated methods,
    1.36 -  but only in single-step methods such as $rule$).
    1.37 +  \emph{unsafe} (i.e.\ not applied blindly without backtracking), while a
    1.38 +  single ``!'' classifies as \emph{safe}, and ``?'' as \emph{extra} (i.e.\ not
    1.39 +  applied in the search-oriented automated methods, but only in single-step
    1.40 +  methods such as $rule$).
    1.41    
    1.42  \item [$iff$] declares equations both as rules for the Simplifier and
    1.43    Classical Reasoner.