--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Thu Nov 01 21:12:13 2001 +0100
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Fri Nov 02 17:55:24 2001 +0100
@@ -279,14 +279,14 @@
also have "... \<le> p (y + a \<cdot> x0)"
proof (rule linorder_cases)
- assume z: "a = Numeral0"
+ assume z: "a = 0"
with vs y a show ?thesis by simp
txt {* In the case @{text "a < 0"}, we use @{text "a\<^sub>1"}
with @{text ya} taken as @{text "y / a"}: *}
next
- assume lz: "a < Numeral0" hence nz: "a \<noteq> Numeral0" by simp
+ assume lz: "a < 0" hence nz: "a \<noteq> 0" by simp
from a1
have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi"
by (rule bspec) (simp!)
@@ -315,7 +315,7 @@
with @{text ya} taken as @{text "y / a"}: *}
next
- assume gz: "Numeral0 < a" hence nz: "a \<noteq> Numeral0" by simp
+ assume gz: "0 < a" hence nz: "a \<noteq> 0" by simp
from a2 have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)"
by (rule bspec) (simp!)