equal
deleted
inserted
replaced
295 by (simp only:) |
295 by (simp only:) |
296 ultimately show ?thesis by blast |
296 ultimately show ?thesis by blast |
297 qed |
297 qed |
298 |
298 |
299 |
299 |
300 subsection \<open>Alternative formulation\<close> |
300 subsection \<open>Alternative formulation\<close> |
301 |
301 |
302 text \<open> |
302 text \<open> |
303 The following alternative formulation of the Hahn-Banach |
303 The following alternative formulation of the Hahn-Banach |
304 Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear |
304 Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear |
305 form @{text f} and a seminorm @{text p} the following inequations |
305 form @{text f} and a seminorm @{text p} the following inequations |