doc-src/IsarRef/generic.tex

   'blast' ('!' ?) nat? (clamod * )
   ;
   ('fast' | 'best' | 'slow' | slowbest) ('!' ?) (clamod * )
   ;
 
-  clamod: (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del') ':' thmrefs
+  clamod: (('intro' | 'elim' | 'dest') (() | '?' | '??') | 'del') ':' thmrefs
   ;
 \end{rail}
 
 \begin{descr}
 \item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac}

 \begin{rail}
   ('force' | 'auto') ('!' ?) (clasimpmod * )
   ;
 
   clasimpmod: ('simp' ('add' | 'del' | 'only') | 'other' |
-    (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del')) ':' thmrefs
+    (('intro' | 'elim' | 'dest') (() | '?' | '??') | 'del')) ':' thmrefs
 \end{rail}
 
 \begin{descr}
 \item [$force$ and $auto$] provide access to Isabelle's combined
   simplification and classical reasoning tactics.  See \texttt{force_tac} and

   iff & : & \isaratt \\
   delrule & : & \isaratt \\
 \end{matharray}
 
 \begin{rail}
-  ('intro' | 'elim' | 'dest') (() | '!' | '!!')
+  ('intro' | 'elim' | 'dest') (() | '?' | '??')
   ;
 \end{rail}
 
 \begin{descr}
 \item [$intro$, $elim$, $dest$] add introduction, elimination, destruct rules,
   respectively.  By default, rules are considered as \emph{safe}, while a
-  single ``!'' classifies as \emph{unsafe}, and ``!!'' as \emph{extra} (i.e.\ 
+  single ``?'' classifies as \emph{unsafe}, and ``??'' as \emph{extra} (i.e.\ 
   not applied in the search-oriented automated methods, but only in
   single-step methods such as $rule$).
   
 \item [$iff$] declares equations both as rewrite rules for the simplifier and
   classical reasoning rules.
 
 \item [$delrule$] deletes introduction or elimination rules from the context.
   Note that destruction rules would have to be turned into elimination rules
   first, e.g.\ by using the $elimify$ attribute.
 \end{descr}
+
 
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "isar-ref"
 %%% End: