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.

     2.1 --- a/doc-src/IsarRef/refcard.tex	Sun Jul 23 11:59:21 2000 +0200
     2.2 +++ b/doc-src/IsarRef/refcard.tex	Sun Jul 23 12:01:05 2000 +0200
     2.3 @@ -127,7 +127,7 @@
     2.4    \multicolumn{2}{l}{\textbf{Declare rules}} \\[0.5ex]
     2.5    $simp$ & declare Simplifier rules \\
     2.6    $split$ & declare Splitter rules \\
     2.7 -  $intro$, $elim$, $dest$ & declare Classical Reasoner rules (also ``?'' or ``??'') \\
     2.8 +  $intro$, $elim$, $dest$ & declare Classical Reasoner rules (also ``!'' or ``?'') \\
     2.9    $iff$ & declare Simplifier + Classical Reasoner rules \\
    2.10    $trans$ & declare calculational rules (general transitivity) \\
    2.11  \end{tabular}

     3.1 --- a/doc-src/Ref/classical.tex	Sun Jul 23 11:59:21 2000 +0200
     3.2 +++ b/doc-src/Ref/classical.tex	Sun Jul 23 12:01:05 2000 +0200
     3.3 @@ -681,7 +681,7 @@
     3.4  current claset by \emph{extra} introduction, elimination, or destruct rules.
     3.5  These provide additional hints for the basic non-automated proof methods of
     3.6  Isabelle/Isar \cite{isabelle-isar-ref}.  The corresponding Isar attributes are
     3.7 -``$intro??$'', ``$elim??$'', and ``$dest??$''.  Note that these extra rules do
     3.8 +``$intro?$'', ``$elim?$'', and ``$dest?$''.  Note that these extra rules do
     3.9  not have any effect on classic Isabelle tactics.
    3.10  
    3.11  

     4.1 --- a/src/HOL/Real/HahnBanach/Aux.thy	Sun Jul 23 11:59:21 2000 +0200
     4.2 +++ b/src/HOL/Real/HahnBanach/Aux.thy	Sun Jul 23 12:01:05 2000 +0200
     4.3 @@ -10,8 +10,8 @@
     4.4  text {* Some existing theorems are declared as extra introduction
     4.5  or elimination rules, respectively. *}
     4.6  
     4.7 -lemmas [intro??] = isLub_isUb
     4.8 -lemmas [intro??] = chainD 
     4.9 +lemmas [intro?] = isLub_isUb
    4.10 +lemmas [intro?] = chainD 
    4.11  lemmas chainE2 = chainD2 [elimify]
    4.12  
    4.13  text_raw {* \medskip *}

     5.1 --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Sun Jul 23 11:59:21 2000 +0200
     5.2 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Sun Jul 23 12:01:05 2000 +0200
     5.3 @@ -30,11 +30,11 @@
     5.4    fix x assume "x \\<in> V" show "|f x| <= c * norm x" by (rule r)
     5.5  qed
     5.6    
     5.7 -lemma continuous_linearform [intro??]: 
     5.8 +lemma continuous_linearform [intro?]: 
     5.9    "is_continuous V norm f ==> is_linearform V f"
    5.10    by (unfold is_continuous_def) force
    5.11  
    5.12 -lemma continuous_bounded [intro??]:
    5.13 +lemma continuous_bounded [intro?]:
    5.14    "is_continuous V norm f 
    5.15    ==> \\<exists>c. \\<forall>x \\<in> V. |f x| <= c * norm x"
    5.16    by (unfold is_continuous_def) force
    5.17 @@ -93,7 +93,7 @@
    5.18  text {* The following lemma states that every continuous linear form
    5.19  on a normed space $(V, \norm{\cdot})$ has a function norm. *}
    5.20  
    5.21 -lemma ex_fnorm [intro??]: 
    5.22 +lemma ex_fnorm [intro?]: 
    5.23    "[| is_normed_vectorspace V norm; is_continuous V norm f|]
    5.24       ==> is_function_norm f V norm \\<parallel>f\\<parallel>V,norm" 
    5.25  proof (unfold function_norm_def is_function_norm_def 
    5.26 @@ -193,7 +193,7 @@
    5.27  
    5.28  text {* The norm of a continuous function is always $\geq 0$. *}
    5.29  
    5.30 -lemma fnorm_ge_zero [intro??]: 
    5.31 +lemma fnorm_ge_zero [intro?]: 
    5.32    "[| is_continuous V norm f; is_normed_vectorspace V norm |]
    5.33     ==> #0 <= \\<parallel>f\\<parallel>V,norm"
    5.34  proof -

     6.1 --- a/src/HOL/Real/HahnBanach/FunctionOrder.thy	Sun Jul 23 11:59:21 2000 +0200
     6.2 +++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Sun Jul 23 12:01:05 2000 +0200
     6.3 @@ -24,16 +24,16 @@
     6.4    graph :: "['a set, 'a => real] => 'a graph "
     6.5    "graph F f == {(x, f x) | x. x \\<in> F}" 
     6.6  
     6.7 -lemma graphI [intro??]: "x \\<in> F ==> (x, f x) \\<in> graph F f"
     6.8 +lemma graphI [intro?]: "x \\<in> F ==> (x, f x) \\<in> graph F f"
     6.9    by (unfold graph_def, intro CollectI exI) force
    6.10  
    6.11 -lemma graphI2 [intro??]: "x \\<in> F ==> \\<exists>t\\<in> (graph F f). t = (x, f x)"
    6.12 +lemma graphI2 [intro?]: "x \\<in> F ==> \\<exists>t\\<in> (graph F f). t = (x, f x)"
    6.13    by (unfold graph_def, force)
    6.14  
    6.15 -lemma graphD1 [intro??]: "(x, y) \\<in> graph F f ==> x \\<in> F"
    6.16 +lemma graphD1 [intro?]: "(x, y) \\<in> graph F f ==> x \\<in> F"
    6.17    by (unfold graph_def, elim CollectE exE) force
    6.18  
    6.19 -lemma graphD2 [intro??]: "(x, y) \\<in> graph H h ==> y = h x"
    6.20 +lemma graphD2 [intro?]: "(x, y) \\<in> graph H h ==> y = h x"
    6.21    by (unfold graph_def, elim CollectE exE) force 
    6.22  
    6.23  subsection {* Functions ordered by domain extension *}
    6.24 @@ -46,11 +46,11 @@
    6.25    ==> graph H h <= graph H' h'"
    6.26    by (unfold graph_def, force)
    6.27  
    6.28 -lemma graph_extD1 [intro??]: 
    6.29 +lemma graph_extD1 [intro?]: 
    6.30    "[| graph H h <= graph H' h'; x \\<in> H |] ==> h x = h' x"
    6.31    by (unfold graph_def, force)
    6.32  
    6.33 -lemma graph_extD2 [intro??]: 
    6.34 +lemma graph_extD2 [intro?]: 
    6.35    "[| graph H h <= graph H' h' |] ==> H <= H'"
    6.36    by (unfold graph_def, force)
    6.37  

     7.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy	Sun Jul 23 11:59:21 2000 +0200
     7.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy	Sun Jul 23 12:01:05 2000 +0200
     7.3 @@ -22,15 +22,15 @@
     7.4   ==> is_linearform V f"
     7.5   by (unfold is_linearform_def) force
     7.6  
     7.7 -lemma linearform_add [intro??]: 
     7.8 +lemma linearform_add [intro?]: 
     7.9    "[| is_linearform V f; x \<in> V; y \<in> V |] ==> f (x + y) = f x + f y"
    7.10    by (unfold is_linearform_def) fast
    7.11  
    7.12 -lemma linearform_mult [intro??]: 
    7.13 +lemma linearform_mult [intro?]: 
    7.14    "[| is_linearform V f; x \<in> V |] ==>  f (a \<cdot> x) = a * (f x)" 
    7.15    by (unfold is_linearform_def) fast
    7.16  
    7.17 -lemma linearform_neg [intro??]:
    7.18 +lemma linearform_neg [intro?]:
    7.19    "[|  is_vectorspace V; is_linearform V f; x \<in> V|] 
    7.20    ==> f (- x) = - f x"
    7.21  proof - 
    7.22 @@ -41,7 +41,7 @@
    7.23    finally show ?thesis .
    7.24  qed
    7.25  
    7.26 -lemma linearform_diff [intro??]: 
    7.27 +lemma linearform_diff [intro?]: 
    7.28    "[| is_vectorspace V; is_linearform V f; x \<in> V; y \<in> V |] 
    7.29    ==> f (x - y) = f x - f y"  
    7.30  proof -
    7.31 @@ -55,7 +55,7 @@
    7.32  
    7.33  text{* Every linear form yields $0$ for the $\zero$ vector.*}
    7.34  
    7.35 -lemma linearform_zero [intro??, simp]: 
    7.36 +lemma linearform_zero [intro?, simp]: 
    7.37    "[| is_vectorspace V; is_linearform V f |] ==> f 0 = #0"
    7.38  proof - 
    7.39    assume "is_vectorspace V" "is_linearform V f"

     8.1 --- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Sun Jul 23 11:59:21 2000 +0200
     8.2 +++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Sun Jul 23 12:01:05 2000 +0200
     8.3 @@ -30,7 +30,7 @@
     8.4    ==> is_seminorm V norm"
     8.5    by (unfold is_seminorm_def, force)
     8.6  
     8.7 -lemma seminorm_ge_zero [intro??]:
     8.8 +lemma seminorm_ge_zero [intro?]:
     8.9    "[| is_seminorm V norm; x \<in> V |] ==> #0 <= norm x"
    8.10    by (unfold is_seminorm_def, force)
    8.11  
    8.12 @@ -86,7 +86,7 @@
    8.13    "\<forall>x \<in> V.  is_seminorm V norm  \<and> (norm x = #0) = (x = 0) 
    8.14    ==> is_norm V norm" by (simp only: is_norm_def)
    8.15  
    8.16 -lemma norm_is_seminorm [intro??]: 
    8.17 +lemma norm_is_seminorm [intro?]: 
    8.18    "[| is_norm V norm; x \<in> V |] ==> is_seminorm V norm"
    8.19    by (unfold is_norm_def, force)
    8.20  
    8.21 @@ -94,7 +94,7 @@
    8.22    "[| is_norm V norm; x \<in> V |] ==> (norm x = #0) = (x = 0)"
    8.23    by (unfold is_norm_def, force)
    8.24  
    8.25 -lemma norm_ge_zero [intro??]:
    8.26 +lemma norm_ge_zero [intro?]:
    8.27    "[|is_norm V norm; x \<in> V |] ==> #0 <= norm x"
    8.28    by (unfold is_norm_def is_seminorm_def, force)
    8.29  
    8.30 @@ -115,19 +115,19 @@
    8.31    ==> is_normed_vectorspace V norm"
    8.32    by (unfold is_normed_vectorspace_def) blast 
    8.33  
    8.34 -lemma normed_vs_vs [intro??]: 
    8.35 +lemma normed_vs_vs [intro?]: 
    8.36    "is_normed_vectorspace V norm ==> is_vectorspace V"
    8.37    by (unfold is_normed_vectorspace_def) force
    8.38  
    8.39 -lemma normed_vs_norm [intro??]: 
    8.40 +lemma normed_vs_norm [intro?]: 
    8.41    "is_normed_vectorspace V norm ==> is_norm V norm"
    8.42    by (unfold is_normed_vectorspace_def, elim conjE)
    8.43  
    8.44 -lemma normed_vs_norm_ge_zero [intro??]: 
    8.45 +lemma normed_vs_norm_ge_zero [intro?]: 
    8.46    "[| is_normed_vectorspace V norm; x \<in> V |] ==> #0 <= norm x"
    8.47    by (unfold is_normed_vectorspace_def, rule, elim conjE)
    8.48  
    8.49 -lemma normed_vs_norm_gt_zero [intro??]: 
    8.50 +lemma normed_vs_norm_gt_zero [intro?]: 
    8.51    "[| is_normed_vectorspace V norm; x \<in> V; x \<noteq> 0 |] ==> #0 < norm x"
    8.52  proof (unfold is_normed_vectorspace_def, elim conjE)
    8.53    assume "x \<in> V" "x \<noteq> 0" "is_vectorspace V" "is_norm V norm"
    8.54 @@ -142,13 +142,13 @@
    8.55    finally show "#0 < norm x" .
    8.56  qed
    8.57  
    8.58 -lemma normed_vs_norm_abs_homogenous [intro??]: 
    8.59 +lemma normed_vs_norm_abs_homogenous [intro?]: 
    8.60    "[| is_normed_vectorspace V norm; x \<in> V |] 
    8.61    ==> norm (a \<cdot> x) = |a| * norm x"
    8.62    by (rule seminorm_abs_homogenous, rule norm_is_seminorm, 
    8.63        rule normed_vs_norm)
    8.64  
    8.65 -lemma normed_vs_norm_subadditive [intro??]: 
    8.66 +lemma normed_vs_norm_subadditive [intro?]: 
    8.67    "[| is_normed_vectorspace V norm; x \<in> V; y \<in> V |] 
    8.68    ==> norm (x + y) <= norm x + norm y"
    8.69    by (rule seminorm_subadditive, rule norm_is_seminorm, 
    8.70 @@ -157,7 +157,7 @@
    8.71  text{* Any subspace of a normed vector space is again a 
    8.72  normed vectorspace.*}
    8.73  
    8.74 -lemma subspace_normed_vs [intro??]: 
    8.75 +lemma subspace_normed_vs [intro?]: 
    8.76    "[| is_vectorspace E; is_subspace F E;
    8.77    is_normed_vectorspace E norm |] ==> is_normed_vectorspace F norm"
    8.78  proof (rule normed_vsI)

     9.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Sun Jul 23 11:59:21 2000 +0200
     9.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Sun Jul 23 12:01:05 2000 +0200
     9.3 @@ -28,25 +28,25 @@
     9.4    assume "0 \<in> U" thus "U \<noteq> {}" by fast
     9.5  qed (simp+)
     9.6  
     9.7 -lemma subspace_not_empty [intro??]: "is_subspace U V ==> U \<noteq> {}"
     9.8 +lemma subspace_not_empty [intro?]: "is_subspace U V ==> U \<noteq> {}"
     9.9    by (unfold is_subspace_def) simp 
    9.10  
    9.11 -lemma subspace_subset [intro??]: "is_subspace U V ==> U <= V"
    9.12 +lemma subspace_subset [intro?]: "is_subspace U V ==> U <= V"
    9.13    by (unfold is_subspace_def) simp
    9.14  
    9.15 -lemma subspace_subsetD [simp, intro??]: 
    9.16 +lemma subspace_subsetD [simp, intro?]: 
    9.17    "[| is_subspace U V; x \<in> U |] ==> x \<in> V"
    9.18    by (unfold is_subspace_def) force
    9.19  
    9.20 -lemma subspace_add_closed [simp, intro??]: 
    9.21 +lemma subspace_add_closed [simp, intro?]: 
    9.22    "[| is_subspace U V; x \<in> U; y \<in> U |] ==> x + y \<in> U"
    9.23    by (unfold is_subspace_def) simp
    9.24  
    9.25 -lemma subspace_mult_closed [simp, intro??]: 
    9.26 +lemma subspace_mult_closed [simp, intro?]: 
    9.27    "[| is_subspace U V; x \<in> U |] ==> a \<cdot> x \<in> U"
    9.28    by (unfold is_subspace_def) simp
    9.29  
    9.30 -lemma subspace_diff_closed [simp, intro??]: 
    9.31 +lemma subspace_diff_closed [simp, intro?]: 
    9.32    "[| is_subspace U V; is_vectorspace V; x \<in> U; y \<in> U |] 
    9.33    ==> x - y \<in> U"
    9.34    by (simp! add: diff_eq1 negate_eq1)
    9.35 @@ -55,7 +55,7 @@
    9.36  zero element in every subspace follows from the non-emptiness 
    9.37  of the carrier set and by vector space laws.*}
    9.38  
    9.39 -lemma zero_in_subspace [intro??]:
    9.40 +lemma zero_in_subspace [intro?]:
    9.41    "[| is_subspace U V; is_vectorspace V |] ==> 0 \<in> U"
    9.42  proof - 
    9.43    assume "is_subspace U V" and v: "is_vectorspace V"
    9.44 @@ -71,14 +71,14 @@
    9.45    qed
    9.46  qed
    9.47  
    9.48 -lemma subspace_neg_closed [simp, intro??]: 
    9.49 +lemma subspace_neg_closed [simp, intro?]: 
    9.50    "[| is_subspace U V; is_vectorspace V; x \<in> U |] ==> - x \<in> U"
    9.51    by (simp add: negate_eq1)
    9.52  
    9.53  text_raw {* \medskip *}
    9.54  text {* Further derived laws: every subspace is a vector space. *}
    9.55  
    9.56 -lemma subspace_vs [intro??]:
    9.57 +lemma subspace_vs [intro?]:
    9.58    "[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U"
    9.59  proof -
    9.60    assume "is_subspace U V" "is_vectorspace V"
    9.61 @@ -144,7 +144,7 @@
    9.62  lemma linD: "x \<in> lin v = (\<exists>a::real. x = a \<cdot> v)"
    9.63    by (unfold lin_def) fast
    9.64  
    9.65 -lemma linI [intro??]: "a \<cdot> x0 \<in> lin x0"
    9.66 +lemma linI [intro?]: "a \<cdot> x0 \<in> lin x0"
    9.67    by (unfold lin_def) fast
    9.68  
    9.69  text {* Every vector is contained in its linear closure. *}
    9.70 @@ -157,7 +157,7 @@
    9.71  
    9.72  text {* Any linear closure is a subspace. *}
    9.73  
    9.74 -lemma lin_subspace [intro??]: 
    9.75 +lemma lin_subspace [intro?]: 
    9.76    "[| is_vectorspace V; x \<in> V |] ==> is_subspace (lin x) V"
    9.77  proof
    9.78    assume "is_vectorspace V" "x \<in> V"
    9.79 @@ -198,7 +198,7 @@
    9.80  
    9.81  text {* Any linear closure is a vector space. *}
    9.82  
    9.83 -lemma lin_vs [intro??]: 
    9.84 +lemma lin_vs [intro?]: 
    9.85    "[| is_vectorspace V; x \<in> V |] ==> is_vectorspace (lin x)"
    9.86  proof (rule subspace_vs)
    9.87    assume "is_vectorspace V" "x \<in> V"
    9.88 @@ -229,13 +229,13 @@
    9.89  
    9.90  lemmas vs_sumE = vs_sumD [RS iffD1, elimify]
    9.91  
    9.92 -lemma vs_sumI [intro??]: 
    9.93 +lemma vs_sumI [intro?]: 
    9.94    "[| x \<in> U; y \<in> V; t= x + y |] ==> t \<in> U + V"
    9.95    by (unfold vs_sum_def) fast
    9.96  
    9.97  text{* $U$ is a subspace of $U + V$. *}
    9.98  
    9.99 -lemma subspace_vs_sum1 [intro??]: 
   9.100 +lemma subspace_vs_sum1 [intro?]: 
   9.101    "[| is_vectorspace U; is_vectorspace V |]
   9.102    ==> is_subspace U (U + V)"
   9.103  proof 
   9.104 @@ -259,7 +259,7 @@
   9.105  
   9.106  text{* The sum of two subspaces is again a subspace.*}
   9.107  
   9.108 -lemma vs_sum_subspace [intro??]: 
   9.109 +lemma vs_sum_subspace [intro?]: 
   9.110    "[| is_subspace U E; is_subspace V E; is_vectorspace E |] 
   9.111    ==> is_subspace (U + V) E"
   9.112  proof 
   9.113 @@ -303,7 +303,7 @@
   9.114  
   9.115  text{* The sum of two subspaces is a vectorspace. *}
   9.116  
   9.117 -lemma vs_sum_vs [intro??]: 
   9.118 +lemma vs_sum_vs [intro?]: 
   9.119    "[| is_subspace U E; is_subspace V E; is_vectorspace E |] 
   9.120    ==> is_vectorspace (U + V)"
   9.121  proof (rule subspace_vs)

    10.1 --- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Sun Jul 23 11:59:21 2000 +0200
    10.2 +++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Sun Jul 23 12:01:05 2000 +0200
    10.3 @@ -70,7 +70,7 @@
    10.4    fix x y z 
    10.5    assume "x \\<in> V" "y \\<in> V" "z \\<in> V"
    10.6      "\\<forall>x \\<in> V. \\<forall>y \\<in> V. \\<forall>z \\<in> V. x + y + z = x + (y + z)"
    10.7 -  thus "x + y + z =  x + (y + z)" by (elim bspec[elimify])
    10.8 +  thus "x + y + z =  x + (y + z)" by blast
    10.9  qed force+
   10.10  
   10.11  text_raw {* \medskip *}
   10.12 @@ -96,22 +96,22 @@
   10.13    "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> x + - y = x - y"
   10.14    by (unfold is_vectorspace_def) simp  
   10.15  
   10.16 -lemma vs_not_empty [intro??]: "is_vectorspace V ==> (V \\<noteq> {})" 
   10.17 +lemma vs_not_empty [intro?]: "is_vectorspace V ==> (V \\<noteq> {})" 
   10.18    by (unfold is_vectorspace_def) simp
   10.19   
   10.20 -lemma vs_add_closed [simp, intro??]: 
   10.21 +lemma vs_add_closed [simp, intro?]: 
   10.22    "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> x + y \\<in> V" 
   10.23    by (unfold is_vectorspace_def) simp
   10.24  
   10.25 -lemma vs_mult_closed [simp, intro??]: 
   10.26 +lemma vs_mult_closed [simp, intro?]: 
   10.27    "[| is_vectorspace V; x \\<in> V |] ==> a \\<cdot> x \\<in> V" 
   10.28    by (unfold is_vectorspace_def) simp
   10.29  
   10.30 -lemma vs_diff_closed [simp, intro??]: 
   10.31 +lemma vs_diff_closed [simp, intro?]: 
   10.32   "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> x - y \\<in> V"
   10.33    by (simp add: diff_eq1 negate_eq1)
   10.34  
   10.35 -lemma vs_neg_closed  [simp, intro??]: 
   10.36 +lemma vs_neg_closed  [simp, intro?]: 
   10.37    "[| is_vectorspace V; x \\<in> V |] ==> - x \\<in> V"
   10.38    by (simp add: negate_eq1)
   10.39  
   10.40 @@ -323,7 +323,7 @@
   10.41      by (simp! only: vs_add_assoc vs_neg_closed)
   10.42    also assume "x + y = x + z"
   10.43    also have "- x + (x + z) = - x + x + z" 
   10.44 -    by (simp! only: vs_add_assoc[RS sym] vs_neg_closed)
   10.45 +    by (simp! only: vs_add_assoc [RS sym] vs_neg_closed)
   10.46    also have "... = z" by (simp!)
   10.47    finally show ?R .
   10.48  qed force

    11.1 --- a/src/Provers/classical.ML	Sun Jul 23 11:59:21 2000 +0200
    11.2 +++ b/src/Provers/classical.ML	Sun Jul 23 12:01:05 2000 +0200
    11.3 @@ -327,17 +327,17 @@
    11.4    is still allowed.*)
    11.5  fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}) = 
    11.6         if mem_thm (th, safeIs) then 
    11.7 -	 warning ("Rule already declared as safe introduction (intro)\n" ^ string_of_thm th)
    11.8 +	 warning ("Rule already declared as safe introduction (intro!)\n" ^ string_of_thm th)
    11.9    else if mem_thm (th, safeEs) then
   11.10 -         warning ("Rule already declared as safe elimination (elim)\n" ^ string_of_thm th)
   11.11 +         warning ("Rule already declared as safe elimination (elim!)\n" ^ string_of_thm th)
   11.12    else if mem_thm (th, hazIs) then 
   11.13 -         warning ("Rule already declared as unsafe introduction (intro?)\n" ^ string_of_thm th)
   11.14 +         warning ("Rule already declared as unsafe introduction (intro)\n" ^ string_of_thm th)
   11.15    else if mem_thm (th, hazEs) then 
   11.16 -         warning ("Rule already declared as unsafe elimination (elim?)\n" ^ string_of_thm th)
   11.17 +         warning ("Rule already declared as unsafe elimination (elim)\n" ^ string_of_thm th)
   11.18    else if mem_thm (th, xtraIs) then 
   11.19 -         warning ("Rule already declared as extra introduction (intro??)\n" ^ string_of_thm th)
   11.20 +         warning ("Rule already declared as extra introduction (intro?)\n" ^ string_of_thm th)
   11.21    else if mem_thm (th, xtraEs) then 
   11.22 -         warning ("Rule already declared as extra elimination (elim??)\n" ^ string_of_thm th)
   11.23 +         warning ("Rule already declared as extra elimination (elim?)\n" ^ string_of_thm th)
   11.24    else ();
   11.25  
   11.26  (*** Safe rules ***)
   11.27 @@ -1030,12 +1030,12 @@
   11.28  
   11.29  val colon = Args.$$$ ":";
   11.30  val query = Args.$$$ "?";
   11.31 -val qquery = Args.$$$ "??";
   11.32 +val bang = Args.$$$ "!";
   11.33  val query_colon = Args.$$$ "?:";
   11.34 -val qquery_colon = Args.$$$ "??:";
   11.35 +val bang_colon = Args.$$$ "!:";
   11.36  
   11.37  fun cla_att change xtra haz safe = Attrib.syntax
   11.38 -  (Scan.lift ((qquery >> K xtra || query >> K haz || Scan.succeed safe) >> change));
   11.39 +  (Scan.lift ((query >> K xtra || bang >> K haz || Scan.succeed safe) >> change));
   11.40  
   11.41  fun cla_attr f g h = (cla_att change_global_cs f g h, cla_att change_local_cs f g h);
   11.42  val del_attr = (Attrib.no_args delrule_global, Attrib.no_args delrule_local);
   11.43 @@ -1146,14 +1146,14 @@
   11.44  (* automatic methods *)
   11.45  
   11.46  val cla_modifiers =
   11.47 - [Args.$$$ destN -- qquery_colon >> K ((I, xtra_dest_local):Method.modifier),
   11.48 -  Args.$$$ destN -- query_colon >> K (I, haz_dest_local),
   11.49 + [Args.$$$ destN -- query_colon >> K ((I, xtra_dest_local):Method.modifier),
   11.50 +  Args.$$$ destN -- bang_colon >> K (I, haz_dest_local),
   11.51    Args.$$$ destN -- colon >> K (I, safe_dest_local),
   11.52 -  Args.$$$ elimN -- qquery_colon >> K (I, xtra_elim_local),
   11.53 -  Args.$$$ elimN -- query_colon >> K (I, haz_elim_local),
   11.54 +  Args.$$$ elimN -- query_colon >> K (I, xtra_elim_local),
   11.55 +  Args.$$$ elimN -- bang_colon >> K (I, haz_elim_local),
   11.56    Args.$$$ elimN -- colon >> K (I, safe_elim_local),
   11.57 -  Args.$$$ introN -- qquery_colon >> K (I, xtra_intro_local),
   11.58 -  Args.$$$ introN -- query_colon >> K (I, haz_intro_local),
   11.59 +  Args.$$$ introN -- query_colon >> K (I, xtra_intro_local),
   11.60 +  Args.$$$ introN -- bang_colon >> K (I, haz_intro_local),
   11.61    Args.$$$ introN -- colon >> K (I, safe_intro_local),
   11.62    Args.$$$ delN -- colon >> K (I, delrule_local)];
   11.63