doc-src/IsarRef/generic.tex
changeset 8203 2fcc6017cb72
parent 8195 af2575a5c5ae
child 8483 b437907f9b26
     1.1 --- a/doc-src/IsarRef/generic.tex	Mon Feb 07 15:28:43 2000 +0100
     1.2 +++ b/doc-src/IsarRef/generic.tex	Mon Feb 07 18:38:51 2000 +0100
     1.3 @@ -389,7 +389,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 @@ -422,7 +422,7 @@
    1.13    ;
    1.14  
    1.15    clasimpmod: ('simp' ('add' | 'del' | 'only') | 'other' |
    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 @@ -452,14 +452,14 @@
    1.22  \end{matharray}
    1.23  
    1.24  \begin{rail}
    1.25 -  ('intro' | 'elim' | 'dest') (() | '!' | '!!')
    1.26 +  ('intro' | 'elim' | 'dest') (() | '?' | '??')
    1.27    ;
    1.28  \end{rail}
    1.29  
    1.30  \begin{descr}
    1.31  \item [$intro$, $elim$, $dest$] add introduction, elimination, destruct rules,
    1.32    respectively.  By default, rules are considered as \emph{safe}, while a
    1.33 -  single ``!'' classifies as \emph{unsafe}, and ``!!'' as \emph{extra} (i.e.\ 
    1.34 +  single ``?'' classifies as \emph{unsafe}, and ``??'' as \emph{extra} (i.e.\ 
    1.35    not applied in the search-oriented automated methods, but only in
    1.36    single-step methods such as $rule$).
    1.37    
    1.38 @@ -471,6 +471,7 @@
    1.39    first, e.g.\ by using the $elimify$ attribute.
    1.40  \end{descr}
    1.41  
    1.42 +
    1.43  %%% Local Variables: 
    1.44  %%% mode: latex
    1.45  %%% TeX-master: "isar-ref"