# HG changeset patch
# User wenzelm
# Date 949945131 -3600
# Node ID 2fcc6017cb72bbfb2cb9075b41ba76d462d7bb8c
# Parent  f32931b936866827f694502b489e119893a0b906
intro/elim/dest attributes: changed ! / !! flags to ? / ??;

diff -r f32931b93686 -r 2fcc6017cb72 NEWS
--- a/NEWS	Mon Feb 07 15:28:43 2000 +0100
+++ b/NEWS	Mon Feb 07 18:38:51 2000 +0100
@@ -12,7 +12,9 @@
 
 *** Isar ***
 
-* names of theorems, assumptions etc. may be natural numbers as well;
+* names of theorems etc. may be natural numbers as well;
+
+* intro/elim/dest attributes: changed ! / !! flags to ? / ??;
 
 * new 'obtain' language element supports generalized existence proofs;
 
diff -r f32931b93686 -r 2fcc6017cb72 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"
diff -r f32931b93686 -r 2fcc6017cb72 doc-src/IsarRef/refcard.tex
--- a/doc-src/IsarRef/refcard.tex	Mon Feb 07 15:28:43 2000 +0100
+++ b/doc-src/IsarRef/refcard.tex	Mon Feb 07 18:38:51 2000 +0100
@@ -112,7 +112,7 @@
 
   \multicolumn{2}{l}{\textbf{Modify context}} \\[0.5ex]
   $simp$ & declare Simplifier 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 f32931b93686 -r 2fcc6017cb72 src/HOL/Real/HahnBanach/Aux.thy
--- a/src/HOL/Real/HahnBanach/Aux.thy	Mon Feb 07 15:28:43 2000 +0100
+++ b/src/HOL/Real/HahnBanach/Aux.thy	Mon Feb 07 18:38:51 2000 +0100
@@ -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 f32931b93686 -r 2fcc6017cb72 src/HOL/Real/HahnBanach/FunctionNorm.thy
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Mon Feb 07 15:28:43 2000 +0100
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Mon Feb 07 18:38:51 2000 +0100
@@ -30,11 +30,11 @@
   fix x; assume "x:V"; show "rabs (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 
   ==> EX c. ALL x:V. rabs (f x) <= c * norm x";
   by (unfold is_continuous_def) force;
@@ -90,7 +90,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 V norm f (function_norm V norm f)"; 
 proof (unfold function_norm_def is_function_norm_def 
@@ -190,7 +190,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|]
    ==> 0r <= function_norm V norm f";
 proof -;
diff -r f32931b93686 -r 2fcc6017cb72 src/HOL/Real/HahnBanach/FunctionOrder.thy
--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy	Mon Feb 07 15:28:43 2000 +0100
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Mon Feb 07 18:38:51 2000 +0100
@@ -24,16 +24,16 @@
   graph :: "['a set, 'a => real] => 'a graph "
   "graph F f == {(x, f x) | x. x:F}"; 
 
-lemma graphI [intro!!]: "x:F ==> (x, f x) : graph F f";
+lemma graphI [intro??]: "x:F ==> (x, f x) : graph F f";
   by (unfold graph_def, intro CollectI exI) force;
 
-lemma graphI2 [intro!!]: "x:F ==> EX t: (graph F f). t = (x, f x)";
+lemma graphI2 [intro??]: "x:F ==> EX t: (graph F f). t = (x, f x)";
   by (unfold graph_def, force);
 
-lemma graphD1 [intro!!]: "(x, y): graph F f ==> x:F";
+lemma graphD1 [intro??]: "(x, y): graph F f ==> x:F";
   by (unfold graph_def, elim CollectE exE) force;
 
-lemma graphD2 [intro!!]: "(x, y): graph H h ==> y = h x";
+lemma graphD2 [intro??]: "(x, y): 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: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 f32931b93686 -r 2fcc6017cb72 src/HOL/Real/HahnBanach/Linearform.thy
--- a/src/HOL/Real/HahnBanach/Linearform.thy	Mon Feb 07 15:28:43 2000 +0100
+++ b/src/HOL/Real/HahnBanach/Linearform.thy	Mon Feb 07 18:38:51 2000 +0100
@@ -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:V; y: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:V |] ==>  f (a <*> 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: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:V; y: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> = 0r"; 
 proof -; 
   assume "is_vectorspace V" "is_linearform V f";
diff -r f32931b93686 -r 2fcc6017cb72 src/HOL/Real/HahnBanach/NormedSpace.thy
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Mon Feb 07 15:28:43 2000 +0100
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Mon Feb 07 18:38:51 2000 +0100
@@ -29,7 +29,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:V |] ==> 0r <= norm x";
   by (unfold is_seminorm_def, force);
 
@@ -85,7 +85,7 @@
   "ALL x: V.  is_seminorm V norm  & (norm x = 0r) = (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:V |] ==> is_seminorm V norm";
   by (unfold is_norm_def, force);
 
@@ -93,7 +93,7 @@
   "[| is_norm V norm; x:V |] ==> (norm x = 0r) = (x = <0>)";
   by (unfold is_norm_def, force);
 
-lemma norm_ge_zero [intro!!]:
+lemma norm_ge_zero [intro??]:
   "[|is_norm V norm; x:V |] ==> 0r <= 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:V |] ==> 0r <= 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:V; x ~= <0> |] ==> 0r < norm x";
 proof (unfold is_normed_vectorspace_def, elim conjE);
   assume "x : V" "x ~= <0>" "is_vectorspace V" "is_norm V norm";
@@ -142,13 +142,13 @@
   finally; show "0r < norm x"; .;
 qed;
 
-lemma normed_vs_norm_rabs_homogenous [intro!!]: 
+lemma normed_vs_norm_rabs_homogenous [intro??]: 
   "[| is_normed_vectorspace V norm; x:V |] 
   ==> norm (a <*> x) = (rabs a) * (norm x)";
   by (rule seminorm_rabs_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:V; y: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_subspace F E; is_vectorspace E; 
   is_normed_vectorspace E norm |] ==> is_normed_vectorspace F norm";
 proof (rule normed_vsI);
diff -r f32931b93686 -r 2fcc6017cb72 src/HOL/Real/HahnBanach/Subspace.thy
--- a/src/HOL/Real/HahnBanach/Subspace.thy	Mon Feb 07 15:28:43 2000 +0100
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Mon Feb 07 18:38:51 2000 +0100
@@ -28,25 +28,25 @@
   assume "<0> : U"; thus "U ~= {}"; by fast;
 qed (simp+);
 
-lemma subspace_not_empty [intro!!]: "is_subspace U V ==> U ~= {}";
+lemma subspace_not_empty [intro??]: "is_subspace U V ==> U ~= {}";
   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:U |] ==> x:V";
   by (unfold is_subspace_def) force;
 
-lemma subspace_add_closed [simp, intro!!]: 
+lemma subspace_add_closed [simp, intro??]: 
   "[| is_subspace U V; x:U; y:U |] ==> x + y : U";
   by (unfold is_subspace_def) simp;
 
-lemma subspace_mult_closed [simp, intro!!]: 
+lemma subspace_mult_closed [simp, intro??]: 
   "[| is_subspace U V; x:U |] ==> a <*> x : 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:U; y:U |] 
   ==> x - y : 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> : 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:U |] ==> - x : 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 : lin v = (EX a::real. x = a <*> v)";
   by (unfold lin_def) fast;
 
-lemma linI [intro!!]: "a <*> x0 : lin x0";
+lemma linI [intro??]: "a <*> x0 : 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:V |] ==> is_subspace (lin x) V";
 proof;
   assume "is_vectorspace V" "x: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:V |] ==> is_vectorspace (lin x)";
 proof (rule subspace_vs);
   assume "is_vectorspace V" "x:V";
@@ -229,13 +229,13 @@
 
 lemmas vs_sumE = vs_sumD [RS iffD1, elimify];
 
-lemma vs_sumI [intro!!]: 
+lemma vs_sumI [intro??]: 
   "[| x:U; y:V; t= x + y |] ==> t : 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 f32931b93686 -r 2fcc6017cb72 src/HOL/Real/HahnBanach/VectorSpace.thy
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Mon Feb 07 15:28:43 2000 +0100
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Mon Feb 07 18:38:51 2000 +0100
@@ -106,22 +106,22 @@
   "[| is_vectorspace V; x:V; y:V |] ==> x + - y = x - y";
   by (unfold is_vectorspace_def) simp;  
 
-lemma vs_not_empty [intro !!]: "is_vectorspace V ==> (V ~= {})"; 
+lemma vs_not_empty [intro??]: "is_vectorspace V ==> (V ~= {})"; 
   by (unfold is_vectorspace_def) simp;
  
-lemma vs_add_closed [simp, intro!!]: 
+lemma vs_add_closed [simp, intro??]: 
   "[| is_vectorspace V; x:V; y:V |] ==> x + y : V"; 
   by (unfold is_vectorspace_def) simp;
 
-lemma vs_mult_closed [simp, intro!!]: 
+lemma vs_mult_closed [simp, intro??]: 
   "[| is_vectorspace V; x:V |] ==> a <*> x : V"; 
   by (unfold is_vectorspace_def) simp;
 
-lemma vs_diff_closed [simp, intro!!]: 
+lemma vs_diff_closed [simp, intro??]: 
  "[| is_vectorspace V; x:V; y:V |] ==> x - y : V";
   by (simp add: diff_eq1 negate_eq1);
 
-lemma vs_neg_closed  [simp, intro!!]: 
+lemma vs_neg_closed  [simp, intro??]: 
   "[| is_vectorspace V; x:V |] ==> - x : V";
   by (simp add: negate_eq1);
 
diff -r f32931b93686 -r 2fcc6017cb72 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Mon Feb 07 15:28:43 2000 +0100
+++ b/src/Provers/classical.ML	Mon Feb 07 18:38:51 2000 +0100
@@ -1021,11 +1021,11 @@
 val delN = "del";
 val delruleN = "delrule";
 
-val bang = Args.$$$ "!";
-val bbang = Args.$$$ "!!";
+val query = Args.$$$ "?";
+val qquery = Args.$$$ "??";
 
 fun cla_att change xtra haz safe = Attrib.syntax
-  (Scan.lift ((bbang >> K xtra || bang >> K haz || Scan.succeed safe) >> change));
+  (Scan.lift ((qquery >> K xtra || query >> 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);
@@ -1134,14 +1134,14 @@
 (* automatic methods *)
 
 val cla_modifiers =
- [Args.$$$ destN -- bbang >> K ((I, xtra_dest_local):Method.modifier),
-  Args.$$$ destN -- bang >> K (I, haz_dest_local),
+ [Args.$$$ destN -- qquery >> K ((I, xtra_dest_local):Method.modifier),
+  Args.$$$ destN -- query >> K (I, haz_dest_local),
   Args.$$$ destN >> K (I, safe_dest_local),
-  Args.$$$ elimN -- bbang >> K (I, xtra_elim_local),
-  Args.$$$ elimN -- bang >> K (I, haz_elim_local),
+  Args.$$$ elimN -- qquery >> K (I, xtra_elim_local),
+  Args.$$$ elimN -- query >> K (I, haz_elim_local),
   Args.$$$ elimN >> K (I, safe_elim_local),
-  Args.$$$ introN -- bbang >> K (I, xtra_intro_local),
-  Args.$$$ introN -- bang >> K (I, haz_intro_local),
+  Args.$$$ introN -- qquery >> K (I, xtra_intro_local),
+  Args.$$$ introN -- query >> K (I, haz_intro_local),
   Args.$$$ introN >> K (I, safe_intro_local),
   Args.$$$ delN >> K (I, delrule_local)];