--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Sun Jul 23 11:59:21 2000 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Sun Jul 23 12:01:05 2000 +0200
@@ -30,11 +30,11 @@
fix x assume "x \\<in> V" show "|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
==> \\<exists>c. \\<forall>x \\<in> V. |f x| <= c * norm x"
by (unfold is_continuous_def) force
@@ -93,7 +93,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 f V norm \\<parallel>f\\<parallel>V,norm"
proof (unfold function_norm_def is_function_norm_def
@@ -193,7 +193,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 |]
==> #0 <= \\<parallel>f\\<parallel>V,norm"
proof -