# HG changeset patch
# User paulson
# Date 978686239 -3600
# Node ID 2781ac7a46196326bd922f81b53cc061b9a674ae
# Parent  ddb433987557243b3a86d0fceff128007545435f
fixed two proofs that were affected by the removal of obsolete rules

diff -r ddb433987557 -r 2781ac7a4619 src/HOL/Real/HahnBanach/Aux.thy
--- a/src/HOL/Real/HahnBanach/Aux.thy	Fri Jan 05 10:15:48 2001 +0100
+++ b/src/HOL/Real/HahnBanach/Aux.thy	Fri Jan 05 10:17:19 2001 +0100
@@ -17,53 +17,44 @@
 
 text {* \medskip Lemmas about sets. *}
 
-lemma Int_singletonD: "A \\<inter> B = {v} \\<Longrightarrow> x \\<in> A \\<Longrightarrow> x \\<in> B \\<Longrightarrow> x = v"
+lemma Int_singletonD: "A \<inter> B = {v} \<Longrightarrow> x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> x = v"
   by (fast elim: equalityE)
 
-lemma set_less_imp_diff_not_empty: "H < E \\<Longrightarrow> \\<exists>x0 \\<in> E. x0 \\<notin> H"
+lemma set_less_imp_diff_not_empty: "H < E \<Longrightarrow> \<exists>x0 \<in> E. x0 \<notin> H"
   by (auto simp add: psubset_eq)
 
 
 text{* \medskip Some lemmas about orders. *}
 
-lemma lt_imp_not_eq: "x < (y::'a::order) \\<Longrightarrow> x \\<noteq> y"
+lemma lt_imp_not_eq: "x < (y::'a::order) \<Longrightarrow> x \<noteq> y"
   by (simp add: order_less_le)
 
 lemma le_noteq_imp_less:
-  "x \\<le> (r::'a::order) \\<Longrightarrow> x \\<noteq> r \\<Longrightarrow> x < r"
+  "x \<le> (r::'a::order) \<Longrightarrow> x \<noteq> r \<Longrightarrow> x < r"
 proof -
-  assume "x \\<le> r" and ne:"x \\<noteq> r"
-  hence "x < r \\<or> x = r" by (simp add: order_le_less)
+  assume "x \<le> r" and ne:"x \<noteq> r"
+  hence "x < r \<or> x = r" by (simp add: order_le_less)
   with ne show ?thesis by simp
 qed
 
 
 text {* \medskip Some lemmas for the reals. *}
 
-lemma real_add_minus_eq: "x - y = (#0::real) \\<Longrightarrow> x = y"
+lemma real_add_minus_eq: "x - y = (#0::real) \<Longrightarrow> x = y"
   by simp
 
 lemma abs_minus_one: "abs (- (#1::real)) = #1"
   by simp
 
 lemma real_mult_le_le_mono1a:
-  "(#0::real) \\<le> z \\<Longrightarrow> x \\<le> y \\<Longrightarrow> z * x  \\<le> z * y"
-proof -
-  assume z: "(#0::real) \\<le> z" and "x \\<le> y"
-  hence "x < y \\<or> x = y" by (auto simp add: order_le_less)
-  thus ?thesis
-  proof
-    assume "x < y" show ?thesis by  (rule real_mult_le_less_mono2) simp
-  next
-    assume "x = y" thus ?thesis by simp
-  qed
-qed
+  "(#0::real) \<le> z \<Longrightarrow> x \<le> y \<Longrightarrow> z * x  \<le> z * y"
+  by (simp add: real_mult_le_mono2)
 
 lemma real_mult_le_le_mono2:
-  "(#0::real) \\<le> z \\<Longrightarrow> x \\<le> y \\<Longrightarrow> x * z \\<le> y * z"
+  "(#0::real) \<le> z \<Longrightarrow> x \<le> y \<Longrightarrow> x * z \<le> y * z"
 proof -
-  assume "(#0::real) \\<le> z"  "x \\<le> y"
-  hence "x < y \\<or> x = y" by (auto simp add: order_le_less)
+  assume "(#0::real) \<le> z"  "x \<le> y"
+  hence "x < y \<or> x = y" by (auto simp add: order_le_less)
   thus ?thesis
   proof
     assume "x < y"
@@ -75,29 +66,29 @@
 qed
 
 lemma real_mult_less_le_anti:
-  "z < (#0::real) \\<Longrightarrow> x \\<le> y \\<Longrightarrow> z * y \\<le> z * x"
+  "z < (#0::real) \<Longrightarrow> x \<le> y \<Longrightarrow> z * y \<le> z * x"
 proof -
-  assume "z < #0"  "x \\<le> y"
+  assume "z < #0"  "x \<le> y"
   hence "#0 < - z" by simp
-  hence "#0 \\<le> - z" by (rule order_less_imp_le)
-  hence "x * (- z) \\<le> y * (- z)"
+  hence "#0 \<le> - z" by (rule order_less_imp_le)
+  hence "x * (- z) \<le> y * (- z)"
     by (rule real_mult_le_le_mono2)
-  hence  "- (x * z) \\<le> - (y * z)"
+  hence  "- (x * z) \<le> - (y * z)"
     by (simp only: real_minus_mult_eq2)
   thus ?thesis by (simp only: real_mult_commute)
 qed
 
 lemma real_mult_less_le_mono:
-  "(#0::real) < z \\<Longrightarrow> x \\<le> y \\<Longrightarrow> z * x \\<le> z * y"
+  "(#0::real) < z \<Longrightarrow> x \<le> y \<Longrightarrow> z * x \<le> z * y"
 proof -
-  assume "#0 < z"  "x \\<le> y"
-  have "#0 \\<le> z" by (rule order_less_imp_le)
-  hence "x * z \\<le> y * z"
+  assume "#0 < z"  "x \<le> y"
+  have "#0 \<le> z" by (rule order_less_imp_le)
+  hence "x * z \<le> y * z"
     by (rule real_mult_le_le_mono2)
   thus ?thesis by (simp only: real_mult_commute)
 qed
 
-lemma real_inverse_gt_zero1: "#0 < (x::real) \\<Longrightarrow> #0 < inverse x"
+lemma real_inverse_gt_zero1: "#0 < (x::real) \<Longrightarrow> #0 < inverse x"
 proof -
   assume "#0 < x"
   have "0 < x" by simp
@@ -105,20 +96,15 @@
   thus ?thesis by simp
 qed
 
-lemma real_mult_inv_right1: "(x::real) \\<noteq> #0 \\<Longrightarrow> x * inverse x = #1"
+lemma real_mult_inv_right1: "(x::real) \<noteq> #0 \<Longrightarrow> x * inverse x = #1"
   by simp
 
-lemma real_mult_inv_left1: "(x::real) \\<noteq> #0 \\<Longrightarrow> inverse x * x = #1"
+lemma real_mult_inv_left1: "(x::real) \<noteq> #0 \<Longrightarrow> inverse x * x = #1"
   by simp
 
 lemma real_le_mult_order1a:
-  "(#0::real) \\<le> x \\<Longrightarrow> #0 \\<le> y \\<Longrightarrow> #0 \\<le> x * y"
-proof -
-  assume "#0 \\<le> x"  "#0 \\<le> y"
-  have "0 \\<le> x \\<Longrightarrow> 0 \\<le> y \\<Longrightarrow> 0 \\<le> x * y"
-    by (rule real_le_mult_order)
-  thus ?thesis by (simp!)
-qed
+  "(#0::real) \<le> x \<Longrightarrow> #0 \<le> y \<Longrightarrow> #0 \<le> x * y"
+  by (simp add: real_0_le_mult_iff)
 
 lemma real_mult_diff_distrib:
   "a * (- x - (y::real)) = - a * x - a * y"
@@ -141,11 +127,11 @@
   finally show ?thesis .
 qed
 
-lemma real_minus_le: "- (x::real) \\<le> y \\<Longrightarrow> - y \\<le> x"
+lemma real_minus_le: "- (x::real) \<le> y \<Longrightarrow> - y \<le> x"
   by simp
 
 lemma real_diff_ineq_swap:
-    "(d::real) - b \\<le> c + a \\<Longrightarrow> - a - b \\<le> c - d"
+    "(d::real) - b \<le> c + a \<Longrightarrow> - a - b \<le> c - d"
   by simp
 
 end