src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
changeset 32960 69916a850301
parent 31795 be3e1cc5005c
child 44887 7ca82df6e951
     1.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -431,7 +431,7 @@
     1.4        from H x have "- x \<in> H" by (rule vectorspace.neg_closed)
     1.5        with r have "h (- x) \<le> p (- x)" ..
     1.6        also have "\<dots> = p x"
     1.7 -	using `seminorm E p` `vectorspace E`
     1.8 +        using `seminorm E p` `vectorspace E`
     1.9        proof (rule seminorm.minus)
    1.10          from x show "x \<in> E" ..
    1.11        qed