doc-src/IsarRef/generic.tex

--- a/doc-src/IsarRef/generic.tex	Mon Feb 07 15:28:43 2000 +0100
+++ b/doc-src/IsarRef/generic.tex	Mon Feb 07 18:38:51 2000 +0100
@@ -389,7 +389,7 @@
   ('fast' | 'best' | 'slow' | slowbest) ('!' ?) (clamod * )
   ;
 
-  clamod: (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del') ':' thmrefs
+  clamod: (('intro' | 'elim' | 'dest') (() | '?' | '??') | 'del') ':' thmrefs
   ;
 \end{rail}
 
@@ -422,7 +422,7 @@
   ;
 
   clasimpmod: ('simp' ('add' | 'del' | 'only') | 'other' |
-    (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del')) ':' thmrefs
+    (('intro' | 'elim' | 'dest') (() | '?' | '??') | 'del')) ':' thmrefs
 \end{rail}
 
 \begin{descr}
@@ -452,14 +452,14 @@
 \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$).
   
@@ -471,6 +471,7 @@
   first, e.g.\ by using the $elimify$ attribute.
 \end{descr}
 
+
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "isar-ref"