src/HOL/Real/HahnBanach/Linearform.thy
 changeset 8203 2fcc6017cb72 parent 7978 1b99ee57d131 child 8703 816d8f6513be
```     1.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy	Mon Feb 07 15:28:43 2000 +0100
1.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy	Mon Feb 07 18:38:51 2000 +0100
1.3 @@ -22,15 +22,15 @@
1.4   ==> is_linearform V f";
1.5   by (unfold is_linearform_def) force;
1.6
1.9    "[| is_linearform V f; x:V; y:V |] ==> f (x + y) = f x + f y";
1.10    by (unfold is_linearform_def) fast;
1.11
1.12 -lemma linearform_mult [intro!!]:
1.13 +lemma linearform_mult [intro??]:
1.14    "[| is_linearform V f; x:V |] ==>  f (a <*> x) = a * (f x)";
1.15    by (unfold is_linearform_def) fast;
1.16
1.17 -lemma linearform_neg [intro!!]:
1.18 +lemma linearform_neg [intro??]:
1.19    "[|  is_vectorspace V; is_linearform V f; x:V|]
1.20    ==> f (- x) = - f x";
1.21  proof -;
1.22 @@ -41,7 +41,7 @@
1.23    finally; show ?thesis; .;
1.24  qed;
1.25
1.26 -lemma linearform_diff [intro!!]:
1.27 +lemma linearform_diff [intro??]:
1.28    "[| is_vectorspace V; is_linearform V f; x:V; y:V |]
1.29    ==> f (x - y) = f x - f y";
1.30  proof -;
1.31 @@ -55,7 +55,7 @@
1.32
1.33  text{* Every linear form yields \$0\$ for the \$\zero\$ vector.*};
1.34
1.35 -lemma linearform_zero [intro!!, simp]:
1.36 +lemma linearform_zero [intro??, simp]:
1.37    "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r";
1.38  proof -;
1.39    assume "is_vectorspace V" "is_linearform V f";
```