summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sat, 26 Apr 2014 14:01:06 +0200 | |

changeset 56749 | e96d6b38649e |

parent 56748 | 10b52ca3b4a2 |

child 56750 | 205dd4439db1 |

tuned spelling;

src/HOL/Hahn_Banach/Hahn_Banach.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Hahn_Banach/Normed_Space.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy Sat Apr 26 14:00:49 2014 +0200 +++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy Sat Apr 26 14:01:06 2014 +0200 @@ -391,7 +391,7 @@ ultimately show "0 \<le> p x" by (simp add: p_def zero_le_mult_iff) - txt {* @{text p} is absolutely homogenous: *} + txt {* @{text p} is absolutely homogeneous: *} show "p (a \<cdot> x) = \<bar>a\<bar> * p x" proof -

--- a/src/HOL/Hahn_Banach/Normed_Space.thy Sat Apr 26 14:00:49 2014 +0200 +++ b/src/HOL/Hahn_Banach/Normed_Space.thy Sat Apr 26 14:01:06 2014 +0200 @@ -13,7 +13,7 @@ text {* A \emph{seminorm} @{text "\<parallel>\<cdot>\<parallel>"} is a function on a real vector space into the reals that has the following properties: it is positive - definite, absolute homogenous and subadditive. + definite, absolute homogeneous and subadditive. *} locale seminorm =