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);