# HG changeset patch
# User wenzelm
# Date 964346465 -7200
# Node ID d3d56e1d2ec1508e24bd22cca64470eb5735f72e
# Parent  e8f6d918fde95624f849d313365e20157dfaeb28
classical atts now intro! / intro / intro?;

diff -r e8f6d918fde9 -r d3d56e1d2ec1 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Sun Jul 23 11:59:21 2000 +0200
+++ b/doc-src/IsarRef/generic.tex	Sun Jul 23 12:01:05 2000 +0200
@@ -550,7 +550,7 @@
   ('fast' | 'best' | 'slow' | slowbest) ('!' ?) (clamod * )
   ;
 
-  clamod: (('intro' | 'elim' | 'dest') (() | '?' | '??') | 'del') ':' thmrefs
+  clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
   ;
 \end{rail}
 
@@ -586,7 +586,7 @@
 
   clasimpmod: ('simp' (() | 'add' | 'del' | 'only') | 'other' |
     ('split' (() | 'add' | 'del')) |
-    (('intro' | 'elim' | 'dest') (() | '?' | '??') | 'del')) ':' thmrefs
+    (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs
 \end{rail}
 
 \begin{descr}
@@ -618,7 +618,7 @@
 \end{matharray}
 
 \begin{rail}
-  ('intro' | 'elim' | 'dest') (() | '?' | '??')
+  ('intro' | 'elim' | 'dest') ('!' | () | '?')
   ;
   'iff' (() | 'add' | 'del')
 \end{rail}
@@ -629,9 +629,10 @@
   \cite{isabelle-ref}.  This is a diagnostic command; $undo$ does not apply.
 \item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
   destruct rules, respectively.  By default, rules are considered as
-  \emph{safe}, while a 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$).
+  \emph{unsafe} (i.e.\ not applied blindly without backtracking), while a
+  single ``!'' classifies as \emph{safe}, 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 rules for the Simplifier and
   Classical Reasoner.
diff -r e8f6d918fde9 -r d3d56e1d2ec1 doc-src/IsarRef/refcard.tex
--- a/doc-src/IsarRef/refcard.tex	Sun Jul 23 11:59:21 2000 +0200
+++ b/doc-src/IsarRef/refcard.tex	Sun Jul 23 12:01:05 2000 +0200
@@ -127,7 +127,7 @@
   \multicolumn{2}{l}{\textbf{Declare rules}} \\[0.5ex]
   $simp$ & declare Simplifier rules \\
   $split$ & declare Splitter rules \\
-  $intro$, $elim$, $dest$ & declare Classical Reasoner rules (also ``?'' or ``??'') \\
+  $intro$, $elim$, $dest$ & declare Classical Reasoner rules (also ``!'' or ``?'') \\
   $iff$ & declare Simplifier + Classical Reasoner rules \\
   $trans$ & declare calculational rules (general transitivity) \\
 \end{tabular}
diff -r e8f6d918fde9 -r d3d56e1d2ec1 doc-src/Ref/classical.tex
--- a/doc-src/Ref/classical.tex	Sun Jul 23 11:59:21 2000 +0200
+++ b/doc-src/Ref/classical.tex	Sun Jul 23 12:01:05 2000 +0200
@@ -681,7 +681,7 @@
 current claset by \emph{extra} introduction, elimination, or destruct rules.
 These provide additional hints for the basic non-automated proof methods of
 Isabelle/Isar \cite{isabelle-isar-ref}.  The corresponding Isar attributes are
-``$intro??$'', ``$elim??$'', and ``$dest??$''.  Note that these extra rules do
+``$intro?$'', ``$elim?$'', and ``$dest?$''.  Note that these extra rules do
 not have any effect on classic Isabelle tactics.
 
 
diff -r e8f6d918fde9 -r d3d56e1d2ec1 src/HOL/Real/HahnBanach/Aux.thy
--- a/src/HOL/Real/HahnBanach/Aux.thy	Sun Jul 23 11:59:21 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Aux.thy	Sun Jul 23 12:01:05 2000 +0200
@@ -10,8 +10,8 @@
 text {* Some existing theorems are declared as extra introduction
 or elimination rules, respectively. *}
 
-lemmas [intro??] = isLub_isUb
-lemmas [intro??] = chainD 
+lemmas [intro?] = isLub_isUb
+lemmas [intro?] = chainD 
 lemmas chainE2 = chainD2 [elimify]
 
 text_raw {* \medskip *}
diff -r e8f6d918fde9 -r d3d56e1d2ec1 src/HOL/Real/HahnBanach/FunctionNorm.thy
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Sun Jul 23 11:59:21 2000 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Sun Jul 23 12:01:05 2000 +0200
@@ -30,11 +30,11 @@
   fix x assume "x \\<in> V" show "|f x| <= c * norm x" by (rule r)
 qed
   
-lemma continuous_linearform [intro??]: 
+lemma continuous_linearform [intro?]: 
   "is_continuous V norm f ==> is_linearform V f"
   by (unfold is_continuous_def) force
 
-lemma continuous_bounded [intro??]:
+lemma continuous_bounded [intro?]:
   "is_continuous V norm f 
   ==> \\<exists>c. \\<forall>x \\<in> V. |f x| <= c * norm x"
   by (unfold is_continuous_def) force
@@ -93,7 +93,7 @@
 text {* The following lemma states that every continuous linear form
 on a normed space $(V, \norm{\cdot})$ has a function norm. *}
 
-lemma ex_fnorm [intro??]: 
+lemma ex_fnorm [intro?]: 
   "[| is_normed_vectorspace V norm; is_continuous V norm f|]
      ==> is_function_norm f V norm \\<parallel>f\\<parallel>V,norm" 
 proof (unfold function_norm_def is_function_norm_def 
@@ -193,7 +193,7 @@
 
 text {* The norm of a continuous function is always $\geq 0$. *}
 
-lemma fnorm_ge_zero [intro??]: 
+lemma fnorm_ge_zero [intro?]: 
   "[| is_continuous V norm f; is_normed_vectorspace V norm |]
    ==> #0 <= \\<parallel>f\\<parallel>V,norm"
 proof -
diff -r e8f6d918fde9 -r d3d56e1d2ec1 src/HOL/Real/HahnBanach/FunctionOrder.thy
--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy	Sun Jul 23 11:59:21 2000 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Sun Jul 23 12:01:05 2000 +0200
@@ -24,16 +24,16 @@
   graph :: "['a set, 'a => real] => 'a graph "
   "graph F f == {(x, f x) | x. x \\<in> F}" 
 
-lemma graphI [intro??]: "x \\<in> F ==> (x, f x) \\<in> graph F f"
+lemma graphI [intro?]: "x \\<in> F ==> (x, f x) \\<in> graph F f"
   by (unfold graph_def, intro CollectI exI) force
 
-lemma graphI2 [intro??]: "x \\<in> F ==> \\<exists>t\\<in> (graph F f). t = (x, f x)"
+lemma graphI2 [intro?]: "x \\<in> F ==> \\<exists>t\\<in> (graph F f). t = (x, f x)"
   by (unfold graph_def, force)
 
-lemma graphD1 [intro??]: "(x, y) \\<in> graph F f ==> x \\<in> F"
+lemma graphD1 [intro?]: "(x, y) \\<in> graph F f ==> x \\<in> F"
   by (unfold graph_def, elim CollectE exE) force
 
-lemma graphD2 [intro??]: "(x, y) \\<in> graph H h ==> y = h x"
+lemma graphD2 [intro?]: "(x, y) \\<in> graph H h ==> y = h x"
   by (unfold graph_def, elim CollectE exE) force 
 
 subsection {* Functions ordered by domain extension *}
@@ -46,11 +46,11 @@
   ==> graph H h <= graph H' h'"
   by (unfold graph_def, force)
 
-lemma graph_extD1 [intro??]: 
+lemma graph_extD1 [intro?]: 
   "[| graph H h <= graph H' h'; x \\<in> H |] ==> h x = h' x"
   by (unfold graph_def, force)
 
-lemma graph_extD2 [intro??]: 
+lemma graph_extD2 [intro?]: 
   "[| graph H h <= graph H' h' |] ==> H <= H'"
   by (unfold graph_def, force)
 
diff -r e8f6d918fde9 -r d3d56e1d2ec1 src/HOL/Real/HahnBanach/Linearform.thy
--- a/src/HOL/Real/HahnBanach/Linearform.thy	Sun Jul 23 11:59:21 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Linearform.thy	Sun Jul 23 12:01:05 2000 +0200
@@ -22,15 +22,15 @@
  ==> is_linearform V f"
  by (unfold is_linearform_def) force
 
-lemma linearform_add [intro??]: 
+lemma linearform_add [intro?]: 
   "[| is_linearform V f; x \<in> V; y \<in> V |] ==> f (x + y) = f x + f y"
   by (unfold is_linearform_def) fast
 
-lemma linearform_mult [intro??]: 
+lemma linearform_mult [intro?]: 
   "[| is_linearform V f; x \<in> V |] ==>  f (a \<cdot> x) = a * (f x)" 
   by (unfold is_linearform_def) fast
 
-lemma linearform_neg [intro??]:
+lemma linearform_neg [intro?]:
   "[|  is_vectorspace V; is_linearform V f; x \<in> V|] 
   ==> f (- x) = - f x"
 proof - 
@@ -41,7 +41,7 @@
   finally show ?thesis .
 qed
 
-lemma linearform_diff [intro??]: 
+lemma linearform_diff [intro?]: 
   "[| is_vectorspace V; is_linearform V f; x \<in> V; y \<in> V |] 
   ==> f (x - y) = f x - f y"  
 proof -
@@ -55,7 +55,7 @@
 
 text{* Every linear form yields $0$ for the $\zero$ vector.*}
 
-lemma linearform_zero [intro??, simp]: 
+lemma linearform_zero [intro?, simp]: 
   "[| is_vectorspace V; is_linearform V f |] ==> f 0 = #0"
 proof - 
   assume "is_vectorspace V" "is_linearform V f"
diff -r e8f6d918fde9 -r d3d56e1d2ec1 src/HOL/Real/HahnBanach/NormedSpace.thy
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Sun Jul 23 11:59:21 2000 +0200
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Sun Jul 23 12:01:05 2000 +0200
@@ -30,7 +30,7 @@
   ==> is_seminorm V norm"
   by (unfold is_seminorm_def, force)
 
-lemma seminorm_ge_zero [intro??]:
+lemma seminorm_ge_zero [intro?]:
   "[| is_seminorm V norm; x \<in> V |] ==> #0 <= norm x"
   by (unfold is_seminorm_def, force)
 
@@ -86,7 +86,7 @@
   "\<forall>x \<in> V.  is_seminorm V norm  \<and> (norm x = #0) = (x = 0) 
   ==> is_norm V norm" by (simp only: is_norm_def)
 
-lemma norm_is_seminorm [intro??]: 
+lemma norm_is_seminorm [intro?]: 
   "[| is_norm V norm; x \<in> V |] ==> is_seminorm V norm"
   by (unfold is_norm_def, force)
 
@@ -94,7 +94,7 @@
   "[| is_norm V norm; x \<in> V |] ==> (norm x = #0) = (x = 0)"
   by (unfold is_norm_def, force)
 
-lemma norm_ge_zero [intro??]:
+lemma norm_ge_zero [intro?]:
   "[|is_norm V norm; x \<in> V |] ==> #0 <= norm x"
   by (unfold is_norm_def is_seminorm_def, force)
 
@@ -115,19 +115,19 @@
   ==> is_normed_vectorspace V norm"
   by (unfold is_normed_vectorspace_def) blast 
 
-lemma normed_vs_vs [intro??]: 
+lemma normed_vs_vs [intro?]: 
   "is_normed_vectorspace V norm ==> is_vectorspace V"
   by (unfold is_normed_vectorspace_def) force
 
-lemma normed_vs_norm [intro??]: 
+lemma normed_vs_norm [intro?]: 
   "is_normed_vectorspace V norm ==> is_norm V norm"
   by (unfold is_normed_vectorspace_def, elim conjE)
 
-lemma normed_vs_norm_ge_zero [intro??]: 
+lemma normed_vs_norm_ge_zero [intro?]: 
   "[| is_normed_vectorspace V norm; x \<in> V |] ==> #0 <= norm x"
   by (unfold is_normed_vectorspace_def, rule, elim conjE)
 
-lemma normed_vs_norm_gt_zero [intro??]: 
+lemma normed_vs_norm_gt_zero [intro?]: 
   "[| is_normed_vectorspace V norm; x \<in> V; x \<noteq> 0 |] ==> #0 < norm x"
 proof (unfold is_normed_vectorspace_def, elim conjE)
   assume "x \<in> V" "x \<noteq> 0" "is_vectorspace V" "is_norm V norm"
@@ -142,13 +142,13 @@
   finally show "#0 < norm x" .
 qed
 
-lemma normed_vs_norm_abs_homogenous [intro??]: 
+lemma normed_vs_norm_abs_homogenous [intro?]: 
   "[| is_normed_vectorspace V norm; x \<in> V |] 
   ==> norm (a \<cdot> x) = |a| * norm x"
   by (rule seminorm_abs_homogenous, rule norm_is_seminorm, 
       rule normed_vs_norm)
 
-lemma normed_vs_norm_subadditive [intro??]: 
+lemma normed_vs_norm_subadditive [intro?]: 
   "[| is_normed_vectorspace V norm; x \<in> V; y \<in> V |] 
   ==> norm (x + y) <= norm x + norm y"
   by (rule seminorm_subadditive, rule norm_is_seminorm, 
@@ -157,7 +157,7 @@
 text{* Any subspace of a normed vector space is again a 
 normed vectorspace.*}
 
-lemma subspace_normed_vs [intro??]: 
+lemma subspace_normed_vs [intro?]: 
   "[| is_vectorspace E; is_subspace F E;
   is_normed_vectorspace E norm |] ==> is_normed_vectorspace F norm"
 proof (rule normed_vsI)
diff -r e8f6d918fde9 -r d3d56e1d2ec1 src/HOL/Real/HahnBanach/Subspace.thy
--- a/src/HOL/Real/HahnBanach/Subspace.thy	Sun Jul 23 11:59:21 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Sun Jul 23 12:01:05 2000 +0200
@@ -28,25 +28,25 @@
   assume "0 \<in> U" thus "U \<noteq> {}" by fast
 qed (simp+)
 
-lemma subspace_not_empty [intro??]: "is_subspace U V ==> U \<noteq> {}"
+lemma subspace_not_empty [intro?]: "is_subspace U V ==> U \<noteq> {}"
   by (unfold is_subspace_def) simp 
 
-lemma subspace_subset [intro??]: "is_subspace U V ==> U <= V"
+lemma subspace_subset [intro?]: "is_subspace U V ==> U <= V"
   by (unfold is_subspace_def) simp
 
-lemma subspace_subsetD [simp, intro??]: 
+lemma subspace_subsetD [simp, intro?]: 
   "[| is_subspace U V; x \<in> U |] ==> x \<in> V"
   by (unfold is_subspace_def) force
 
-lemma subspace_add_closed [simp, intro??]: 
+lemma subspace_add_closed [simp, intro?]: 
   "[| is_subspace U V; x \<in> U; y \<in> U |] ==> x + y \<in> U"
   by (unfold is_subspace_def) simp
 
-lemma subspace_mult_closed [simp, intro??]: 
+lemma subspace_mult_closed [simp, intro?]: 
   "[| is_subspace U V; x \<in> U |] ==> a \<cdot> x \<in> U"
   by (unfold is_subspace_def) simp
 
-lemma subspace_diff_closed [simp, intro??]: 
+lemma subspace_diff_closed [simp, intro?]: 
   "[| is_subspace U V; is_vectorspace V; x \<in> U; y \<in> U |] 
   ==> x - y \<in> U"
   by (simp! add: diff_eq1 negate_eq1)
@@ -55,7 +55,7 @@
 zero element in every subspace follows from the non-emptiness 
 of the carrier set and by vector space laws.*}
 
-lemma zero_in_subspace [intro??]:
+lemma zero_in_subspace [intro?]:
   "[| is_subspace U V; is_vectorspace V |] ==> 0 \<in> U"
 proof - 
   assume "is_subspace U V" and v: "is_vectorspace V"
@@ -71,14 +71,14 @@
   qed
 qed
 
-lemma subspace_neg_closed [simp, intro??]: 
+lemma subspace_neg_closed [simp, intro?]: 
   "[| is_subspace U V; is_vectorspace V; x \<in> U |] ==> - x \<in> U"
   by (simp add: negate_eq1)
 
 text_raw {* \medskip *}
 text {* Further derived laws: every subspace is a vector space. *}
 
-lemma subspace_vs [intro??]:
+lemma subspace_vs [intro?]:
   "[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U"
 proof -
   assume "is_subspace U V" "is_vectorspace V"
@@ -144,7 +144,7 @@
 lemma linD: "x \<in> lin v = (\<exists>a::real. x = a \<cdot> v)"
   by (unfold lin_def) fast
 
-lemma linI [intro??]: "a \<cdot> x0 \<in> lin x0"
+lemma linI [intro?]: "a \<cdot> x0 \<in> lin x0"
   by (unfold lin_def) fast
 
 text {* Every vector is contained in its linear closure. *}
@@ -157,7 +157,7 @@
 
 text {* Any linear closure is a subspace. *}
 
-lemma lin_subspace [intro??]: 
+lemma lin_subspace [intro?]: 
   "[| is_vectorspace V; x \<in> V |] ==> is_subspace (lin x) V"
 proof
   assume "is_vectorspace V" "x \<in> V"
@@ -198,7 +198,7 @@
 
 text {* Any linear closure is a vector space. *}
 
-lemma lin_vs [intro??]: 
+lemma lin_vs [intro?]: 
   "[| is_vectorspace V; x \<in> V |] ==> is_vectorspace (lin x)"
 proof (rule subspace_vs)
   assume "is_vectorspace V" "x \<in> V"
@@ -229,13 +229,13 @@
 
 lemmas vs_sumE = vs_sumD [RS iffD1, elimify]
 
-lemma vs_sumI [intro??]: 
+lemma vs_sumI [intro?]: 
   "[| x \<in> U; y \<in> V; t= x + y |] ==> t \<in> U + V"
   by (unfold vs_sum_def) fast
 
 text{* $U$ is a subspace of $U + V$. *}
 
-lemma subspace_vs_sum1 [intro??]: 
+lemma subspace_vs_sum1 [intro?]: 
   "[| is_vectorspace U; is_vectorspace V |]
   ==> is_subspace U (U + V)"
 proof 
@@ -259,7 +259,7 @@
 
 text{* The sum of two subspaces is again a subspace.*}
 
-lemma vs_sum_subspace [intro??]: 
+lemma vs_sum_subspace [intro?]: 
   "[| is_subspace U E; is_subspace V E; is_vectorspace E |] 
   ==> is_subspace (U + V) E"
 proof 
@@ -303,7 +303,7 @@
 
 text{* The sum of two subspaces is a vectorspace. *}
 
-lemma vs_sum_vs [intro??]: 
+lemma vs_sum_vs [intro?]: 
   "[| is_subspace U E; is_subspace V E; is_vectorspace E |] 
   ==> is_vectorspace (U + V)"
 proof (rule subspace_vs)
diff -r e8f6d918fde9 -r d3d56e1d2ec1 src/HOL/Real/HahnBanach/VectorSpace.thy
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Sun Jul 23 11:59:21 2000 +0200
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Sun Jul 23 12:01:05 2000 +0200
@@ -70,7 +70,7 @@
   fix x y z 
   assume "x \\<in> V" "y \\<in> V" "z \\<in> V"
     "\\<forall>x \\<in> V. \\<forall>y \\<in> V. \\<forall>z \\<in> V. x + y + z = x + (y + z)"
-  thus "x + y + z =  x + (y + z)" by (elim bspec[elimify])
+  thus "x + y + z =  x + (y + z)" by blast
 qed force+
 
 text_raw {* \medskip *}
@@ -96,22 +96,22 @@
   "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> x + - y = x - y"
   by (unfold is_vectorspace_def) simp  
 
-lemma vs_not_empty [intro??]: "is_vectorspace V ==> (V \\<noteq> {})" 
+lemma vs_not_empty [intro?]: "is_vectorspace V ==> (V \\<noteq> {})" 
   by (unfold is_vectorspace_def) simp
  
-lemma vs_add_closed [simp, intro??]: 
+lemma vs_add_closed [simp, intro?]: 
   "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> x + y \\<in> V" 
   by (unfold is_vectorspace_def) simp
 
-lemma vs_mult_closed [simp, intro??]: 
+lemma vs_mult_closed [simp, intro?]: 
   "[| is_vectorspace V; x \\<in> V |] ==> a \\<cdot> x \\<in> V" 
   by (unfold is_vectorspace_def) simp
 
-lemma vs_diff_closed [simp, intro??]: 
+lemma vs_diff_closed [simp, intro?]: 
  "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> x - y \\<in> V"
   by (simp add: diff_eq1 negate_eq1)
 
-lemma vs_neg_closed  [simp, intro??]: 
+lemma vs_neg_closed  [simp, intro?]: 
   "[| is_vectorspace V; x \\<in> V |] ==> - x \\<in> V"
   by (simp add: negate_eq1)
 
@@ -323,7 +323,7 @@
     by (simp! only: vs_add_assoc vs_neg_closed)
   also assume "x + y = x + z"
   also have "- x + (x + z) = - x + x + z" 
-    by (simp! only: vs_add_assoc[RS sym] vs_neg_closed)
+    by (simp! only: vs_add_assoc [RS sym] vs_neg_closed)
   also have "... = z" by (simp!)
   finally show ?R .
 qed force
diff -r e8f6d918fde9 -r d3d56e1d2ec1 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sun Jul 23 11:59:21 2000 +0200
+++ b/src/Provers/classical.ML	Sun Jul 23 12:01:05 2000 +0200
@@ -327,17 +327,17 @@
   is still allowed.*)
 fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}) = 
        if mem_thm (th, safeIs) then 
-	 warning ("Rule already declared as safe introduction (intro)\n" ^ string_of_thm th)
+	 warning ("Rule already declared as safe introduction (intro!)\n" ^ string_of_thm th)
   else if mem_thm (th, safeEs) then
-         warning ("Rule already declared as safe elimination (elim)\n" ^ string_of_thm th)
+         warning ("Rule already declared as safe elimination (elim!)\n" ^ string_of_thm th)
   else if mem_thm (th, hazIs) then 
-         warning ("Rule already declared as unsafe introduction (intro?)\n" ^ string_of_thm th)
+         warning ("Rule already declared as unsafe introduction (intro)\n" ^ string_of_thm th)
   else if mem_thm (th, hazEs) then 
-         warning ("Rule already declared as unsafe elimination (elim?)\n" ^ string_of_thm th)
+         warning ("Rule already declared as unsafe elimination (elim)\n" ^ string_of_thm th)
   else if mem_thm (th, xtraIs) then 
-         warning ("Rule already declared as extra introduction (intro??)\n" ^ string_of_thm th)
+         warning ("Rule already declared as extra introduction (intro?)\n" ^ string_of_thm th)
   else if mem_thm (th, xtraEs) then 
-         warning ("Rule already declared as extra elimination (elim??)\n" ^ string_of_thm th)
+         warning ("Rule already declared as extra elimination (elim?)\n" ^ string_of_thm th)
   else ();
 
 (*** Safe rules ***)
@@ -1030,12 +1030,12 @@
 
 val colon = Args.$$$ ":";
 val query = Args.$$$ "?";
-val qquery = Args.$$$ "??";
+val bang = Args.$$$ "!";
 val query_colon = Args.$$$ "?:";
-val qquery_colon = Args.$$$ "??:";
+val bang_colon = Args.$$$ "!:";
 
 fun cla_att change xtra haz safe = Attrib.syntax
-  (Scan.lift ((qquery >> K xtra || query >> K haz || Scan.succeed safe) >> change));
+  (Scan.lift ((query >> K xtra || bang >> K haz || Scan.succeed safe) >> change));
 
 fun cla_attr f g h = (cla_att change_global_cs f g h, cla_att change_local_cs f g h);
 val del_attr = (Attrib.no_args delrule_global, Attrib.no_args delrule_local);
@@ -1146,14 +1146,14 @@
 (* automatic methods *)
 
 val cla_modifiers =
- [Args.$$$ destN -- qquery_colon >> K ((I, xtra_dest_local):Method.modifier),
-  Args.$$$ destN -- query_colon >> K (I, haz_dest_local),
+ [Args.$$$ destN -- query_colon >> K ((I, xtra_dest_local):Method.modifier),
+  Args.$$$ destN -- bang_colon >> K (I, haz_dest_local),
   Args.$$$ destN -- colon >> K (I, safe_dest_local),
-  Args.$$$ elimN -- qquery_colon >> K (I, xtra_elim_local),
-  Args.$$$ elimN -- query_colon >> K (I, haz_elim_local),
+  Args.$$$ elimN -- query_colon >> K (I, xtra_elim_local),
+  Args.$$$ elimN -- bang_colon >> K (I, haz_elim_local),
   Args.$$$ elimN -- colon >> K (I, safe_elim_local),
-  Args.$$$ introN -- qquery_colon >> K (I, xtra_intro_local),
-  Args.$$$ introN -- query_colon >> K (I, haz_intro_local),
+  Args.$$$ introN -- query_colon >> K (I, xtra_intro_local),
+  Args.$$$ introN -- bang_colon >> K (I, haz_intro_local),
   Args.$$$ introN -- colon >> K (I, safe_intro_local),
   Args.$$$ delN -- colon >> K (I, delrule_local)];