intro/elim/dest attributes: changed ! / !! flags to ? / ??;
authorwenzelm
Mon Feb 07 18:38:51 2000 +0100 (2000-02-07)
changeset 82032fcc6017cb72
parent 8202 f32931b93686
child 8204 b2a4a3d86b73
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
NEWS
doc-src/IsarRef/generic.tex
doc-src/IsarRef/refcard.tex
src/HOL/Real/HahnBanach/Aux.thy
src/HOL/Real/HahnBanach/FunctionNorm.thy
src/HOL/Real/HahnBanach/FunctionOrder.thy
src/HOL/Real/HahnBanach/Linearform.thy
src/HOL/Real/HahnBanach/NormedSpace.thy
src/HOL/Real/HahnBanach/Subspace.thy
src/HOL/Real/HahnBanach/VectorSpace.thy
src/Provers/classical.ML
     1.1 --- a/NEWS	Mon Feb 07 15:28:43 2000 +0100
     1.2 +++ b/NEWS	Mon Feb 07 18:38:51 2000 +0100
     1.3 @@ -12,7 +12,9 @@
     1.4  
     1.5  *** Isar ***
     1.6  
     1.7 -* names of theorems, assumptions etc. may be natural numbers as well;
     1.8 +* names of theorems etc. may be natural numbers as well;
     1.9 +
    1.10 +* intro/elim/dest attributes: changed ! / !! flags to ? / ??;
    1.11  
    1.12  * new 'obtain' language element supports generalized existence proofs;
    1.13  
     2.1 --- a/doc-src/IsarRef/generic.tex	Mon Feb 07 15:28:43 2000 +0100
     2.2 +++ b/doc-src/IsarRef/generic.tex	Mon Feb 07 18:38:51 2000 +0100
     2.3 @@ -389,7 +389,7 @@
     2.4    ('fast' | 'best' | 'slow' | slowbest) ('!' ?) (clamod * )
     2.5    ;
     2.6  
     2.7 -  clamod: (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del') ':' thmrefs
     2.8 +  clamod: (('intro' | 'elim' | 'dest') (() | '?' | '??') | 'del') ':' thmrefs
     2.9    ;
    2.10  \end{rail}
    2.11  
    2.12 @@ -422,7 +422,7 @@
    2.13    ;
    2.14  
    2.15    clasimpmod: ('simp' ('add' | 'del' | 'only') | 'other' |
    2.16 -    (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del')) ':' thmrefs
    2.17 +    (('intro' | 'elim' | 'dest') (() | '?' | '??') | 'del')) ':' thmrefs
    2.18  \end{rail}
    2.19  
    2.20  \begin{descr}
    2.21 @@ -452,14 +452,14 @@
    2.22  \end{matharray}
    2.23  
    2.24  \begin{rail}
    2.25 -  ('intro' | 'elim' | 'dest') (() | '!' | '!!')
    2.26 +  ('intro' | 'elim' | 'dest') (() | '?' | '??')
    2.27    ;
    2.28  \end{rail}
    2.29  
    2.30  \begin{descr}
    2.31  \item [$intro$, $elim$, $dest$] add introduction, elimination, destruct rules,
    2.32    respectively.  By default, rules are considered as \emph{safe}, while a
    2.33 -  single ``!'' classifies as \emph{unsafe}, and ``!!'' as \emph{extra} (i.e.\ 
    2.34 +  single ``?'' classifies as \emph{unsafe}, and ``??'' as \emph{extra} (i.e.\ 
    2.35    not applied in the search-oriented automated methods, but only in
    2.36    single-step methods such as $rule$).
    2.37    
    2.38 @@ -471,6 +471,7 @@
    2.39    first, e.g.\ by using the $elimify$ attribute.
    2.40  \end{descr}
    2.41  
    2.42 +
    2.43  %%% Local Variables: 
    2.44  %%% mode: latex
    2.45  %%% TeX-master: "isar-ref"
     3.1 --- a/doc-src/IsarRef/refcard.tex	Mon Feb 07 15:28:43 2000 +0100
     3.2 +++ b/doc-src/IsarRef/refcard.tex	Mon Feb 07 18:38:51 2000 +0100
     3.3 @@ -112,7 +112,7 @@
     3.4  
     3.5    \multicolumn{2}{l}{\textbf{Modify context}} \\[0.5ex]
     3.6    $simp$ & declare Simplifier rules \\
     3.7 -  $intro$, $elim$, $dest$ & declare Classical Reasoner rules (also ``$!$'' or ``$!!$'') \\
     3.8 +  $intro$, $elim$, $dest$ & declare Classical Reasoner rules (also ``?'' or ``??'') \\
     3.9    $iff$ & declare Simplifier + Classical Reasoner rules \\
    3.10    $trans$ & declare calculational rules (general transitivity) \\
    3.11  \end{tabular}
     4.1 --- a/src/HOL/Real/HahnBanach/Aux.thy	Mon Feb 07 15:28:43 2000 +0100
     4.2 +++ b/src/HOL/Real/HahnBanach/Aux.thy	Mon Feb 07 18:38:51 2000 +0100
     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	Mon Feb 07 15:28:43 2000 +0100
     5.2 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Mon Feb 07 18:38:51 2000 +0100
     5.3 @@ -30,11 +30,11 @@
     5.4    fix x; assume "x:V"; show "rabs (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    ==> EX c. ALL x:V. rabs (f x) <= c * norm x";
    5.16    by (unfold is_continuous_def) force;
    5.17 @@ -90,7 +90,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 V norm f (function_norm V norm f)"; 
    5.25  proof (unfold function_norm_def is_function_norm_def 
    5.26 @@ -190,7 +190,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     ==> 0r <= function_norm V norm f";
    5.34  proof -;
     6.1 --- a/src/HOL/Real/HahnBanach/FunctionOrder.thy	Mon Feb 07 15:28:43 2000 +0100
     6.2 +++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Mon Feb 07 18:38:51 2000 +0100
     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:F}"; 
     6.6  
     6.7 -lemma graphI [intro!!]: "x:F ==> (x, f x) : graph F f";
     6.8 +lemma graphI [intro??]: "x:F ==> (x, f x) : graph F f";
     6.9    by (unfold graph_def, intro CollectI exI) force;
    6.10  
    6.11 -lemma graphI2 [intro!!]: "x:F ==> EX t: (graph F f). t = (x, f x)";
    6.12 +lemma graphI2 [intro??]: "x:F ==> EX t: (graph F f). t = (x, f x)";
    6.13    by (unfold graph_def, force);
    6.14  
    6.15 -lemma graphD1 [intro!!]: "(x, y): graph F f ==> x:F";
    6.16 +lemma graphD1 [intro??]: "(x, y): graph F f ==> x:F";
    6.17    by (unfold graph_def, elim CollectE exE) force;
    6.18  
    6.19 -lemma graphD2 [intro!!]: "(x, y): graph H h ==> y = h x";
    6.20 +lemma graphD2 [intro??]: "(x, y): 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: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	Mon Feb 07 15:28:43 2000 +0100
     7.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy	Mon Feb 07 18:38:51 2000 +0100
     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:V; y: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:V |] ==>  f (a <*> 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: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:V; y: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> = 0r"; 
    7.38  proof -; 
    7.39    assume "is_vectorspace V" "is_linearform V f";
     8.1 --- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Mon Feb 07 15:28:43 2000 +0100
     8.2 +++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Mon Feb 07 18:38:51 2000 +0100
     8.3 @@ -29,7 +29,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:V |] ==> 0r <= norm x";
    8.10    by (unfold is_seminorm_def, force);
    8.11  
    8.12 @@ -85,7 +85,7 @@
    8.13    "ALL x: V.  is_seminorm V norm  & (norm x = 0r) = (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:V |] ==> is_seminorm V norm";
    8.19    by (unfold is_norm_def, force);
    8.20  
    8.21 @@ -93,7 +93,7 @@
    8.22    "[| is_norm V norm; x:V |] ==> (norm x = 0r) = (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:V |] ==> 0r <= 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:V |] ==> 0r <= 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:V; x ~= <0> |] ==> 0r < norm x";
    8.52  proof (unfold is_normed_vectorspace_def, elim conjE);
    8.53    assume "x : V" "x ~= <0>" "is_vectorspace V" "is_norm V norm";
    8.54 @@ -142,13 +142,13 @@
    8.55    finally; show "0r < norm x"; .;
    8.56  qed;
    8.57  
    8.58 -lemma normed_vs_norm_rabs_homogenous [intro!!]: 
    8.59 +lemma normed_vs_norm_rabs_homogenous [intro??]: 
    8.60    "[| is_normed_vectorspace V norm; x:V |] 
    8.61    ==> norm (a <*> x) = (rabs a) * (norm x)";
    8.62    by (rule seminorm_rabs_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:V; y: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_subspace F E; is_vectorspace 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	Mon Feb 07 15:28:43 2000 +0100
     9.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Mon Feb 07 18:38:51 2000 +0100
     9.3 @@ -28,25 +28,25 @@
     9.4    assume "<0> : U"; thus "U ~= {}"; by fast;
     9.5  qed (simp+);
     9.6  
     9.7 -lemma subspace_not_empty [intro!!]: "is_subspace U V ==> U ~= {}";
     9.8 +lemma subspace_not_empty [intro??]: "is_subspace U V ==> U ~= {}";
     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:U |] ==> x: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:U; y:U |] ==> x + y : 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:U |] ==> a <*> x : 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:U; y:U |] 
    9.33    ==> x - y : 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> : 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:U |] ==> - x : 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 : lin v = (EX a::real. x = a <*> v)";
    9.63    by (unfold lin_def) fast;
    9.64  
    9.65 -lemma linI [intro!!]: "a <*> x0 : lin x0";
    9.66 +lemma linI [intro??]: "a <*> x0 : 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:V |] ==> is_subspace (lin x) V";
    9.77  proof;
    9.78    assume "is_vectorspace V" "x: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:V |] ==> is_vectorspace (lin x)";
    9.86  proof (rule subspace_vs);
    9.87    assume "is_vectorspace V" "x: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:U; y:V; t= x + y |] ==> t : 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	Mon Feb 07 15:28:43 2000 +0100
    10.2 +++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Mon Feb 07 18:38:51 2000 +0100
    10.3 @@ -106,22 +106,22 @@
    10.4    "[| is_vectorspace V; x:V; y:V |] ==> x + - y = x - y";
    10.5    by (unfold is_vectorspace_def) simp;  
    10.6  
    10.7 -lemma vs_not_empty [intro !!]: "is_vectorspace V ==> (V ~= {})"; 
    10.8 +lemma vs_not_empty [intro??]: "is_vectorspace V ==> (V ~= {})"; 
    10.9    by (unfold is_vectorspace_def) simp;
   10.10   
   10.11 -lemma vs_add_closed [simp, intro!!]: 
   10.12 +lemma vs_add_closed [simp, intro??]: 
   10.13    "[| is_vectorspace V; x:V; y:V |] ==> x + y : V"; 
   10.14    by (unfold is_vectorspace_def) simp;
   10.15  
   10.16 -lemma vs_mult_closed [simp, intro!!]: 
   10.17 +lemma vs_mult_closed [simp, intro??]: 
   10.18    "[| is_vectorspace V; x:V |] ==> a <*> x : V"; 
   10.19    by (unfold is_vectorspace_def) simp;
   10.20  
   10.21 -lemma vs_diff_closed [simp, intro!!]: 
   10.22 +lemma vs_diff_closed [simp, intro??]: 
   10.23   "[| is_vectorspace V; x:V; y:V |] ==> x - y : V";
   10.24    by (simp add: diff_eq1 negate_eq1);
   10.25  
   10.26 -lemma vs_neg_closed  [simp, intro!!]: 
   10.27 +lemma vs_neg_closed  [simp, intro??]: 
   10.28    "[| is_vectorspace V; x:V |] ==> - x : V";
   10.29    by (simp add: negate_eq1);
   10.30  
    11.1 --- a/src/Provers/classical.ML	Mon Feb 07 15:28:43 2000 +0100
    11.2 +++ b/src/Provers/classical.ML	Mon Feb 07 18:38:51 2000 +0100
    11.3 @@ -1021,11 +1021,11 @@
    11.4  val delN = "del";
    11.5  val delruleN = "delrule";
    11.6  
    11.7 -val bang = Args.$$$ "!";
    11.8 -val bbang = Args.$$$ "!!";
    11.9 +val query = Args.$$$ "?";
   11.10 +val qquery = Args.$$$ "??";
   11.11  
   11.12  fun cla_att change xtra haz safe = Attrib.syntax
   11.13 -  (Scan.lift ((bbang >> K xtra || bang >> K haz || Scan.succeed safe) >> change));
   11.14 +  (Scan.lift ((qquery >> K xtra || query >> K haz || Scan.succeed safe) >> change));
   11.15  
   11.16  fun cla_attr f g h = (cla_att change_global_cs f g h, cla_att change_local_cs f g h);
   11.17  val del_attr = (Attrib.no_args delrule_global, Attrib.no_args delrule_local);
   11.18 @@ -1134,14 +1134,14 @@
   11.19  (* automatic methods *)
   11.20  
   11.21  val cla_modifiers =
   11.22 - [Args.$$$ destN -- bbang >> K ((I, xtra_dest_local):Method.modifier),
   11.23 -  Args.$$$ destN -- bang >> K (I, haz_dest_local),
   11.24 + [Args.$$$ destN -- qquery >> K ((I, xtra_dest_local):Method.modifier),
   11.25 +  Args.$$$ destN -- query >> K (I, haz_dest_local),
   11.26    Args.$$$ destN >> K (I, safe_dest_local),
   11.27 -  Args.$$$ elimN -- bbang >> K (I, xtra_elim_local),
   11.28 -  Args.$$$ elimN -- bang >> K (I, haz_elim_local),
   11.29 +  Args.$$$ elimN -- qquery >> K (I, xtra_elim_local),
   11.30 +  Args.$$$ elimN -- query >> K (I, haz_elim_local),
   11.31    Args.$$$ elimN >> K (I, safe_elim_local),
   11.32 -  Args.$$$ introN -- bbang >> K (I, xtra_intro_local),
   11.33 -  Args.$$$ introN -- bang >> K (I, haz_intro_local),
   11.34 +  Args.$$$ introN -- qquery >> K (I, xtra_intro_local),
   11.35 +  Args.$$$ introN -- query >> K (I, haz_intro_local),
   11.36    Args.$$$ introN >> K (I, safe_intro_local),
   11.37    Args.$$$ delN >> K (I, delrule_local)];
   11.38