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.7 -lemma linearform_add [intro!!]: 
     1.8 +lemma linearform_add [intro??]: 
     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";