# HG changeset patch
# User wenzelm
# Date 1205868811 -3600
# Node ID 9e9e67e33557251703df13f4f3aecdc460a0b188
# Parent  cb3badaa192eaeaba1f7e4cef4ece7159dee0a18
removed redundant less_trans, less_linear, le_imp_less_or_eq, le_less_trans, less_le_trans (cf. Orderings.thy);

diff -r cb3badaa192e -r 9e9e67e33557 src/HOL/HoareParallel/Gar_Coll.thy
--- a/src/HOL/HoareParallel/Gar_Coll.thy	Tue Mar 18 20:33:29 2008 +0100
+++ b/src/HOL/HoareParallel/Gar_Coll.thy	Tue Mar 18 20:33:31 2008 +0100
@@ -185,7 +185,7 @@
   apply (erule_tac x=i in allE , erule (1) notE impE)
   apply simp
   apply clarify
-  apply (drule Nat.le_imp_less_or_eq)
+  apply (drule_tac y = r in le_imp_less_or_eq)
   apply (erule disjE)
    apply (subgoal_tac "Suc (ind x)\<le>r")
     apply fast
@@ -276,7 +276,7 @@
    apply (erule_tac x=i in allE , erule (1) notE impE)
    apply simp
    apply clarify
-   apply (drule Nat.le_imp_less_or_eq)
+   apply (drule_tac y = r in le_imp_less_or_eq)
    apply (erule disjE)
     apply (subgoal_tac "Suc (ind x)\<le>r")
      apply fast
@@ -309,7 +309,7 @@
  apply (erule_tac x=i in allE , erule (1) notE impE)
  apply simp
  apply clarify
- apply (drule Nat.le_imp_less_or_eq)
+ apply (drule_tac y = r in le_imp_less_or_eq)
  apply (erule disjE)
   apply (subgoal_tac "Suc (ind x)\<le>r")
    apply fast
diff -r cb3badaa192e -r 9e9e67e33557 src/HOL/HoareParallel/Graph.thy
--- a/src/HOL/HoareParallel/Graph.thy	Tue Mar 18 20:33:29 2008 +0100
+++ b/src/HOL/HoareParallel/Graph.thy	Tue Mar 18 20:33:31 2008 +0100
@@ -336,7 +336,7 @@
  apply(erule_tac P = "\<lambda>i. i < Suc nat \<longrightarrow> ?P i" and x = "nat" in allE)
  apply simp
  apply(case_tac "j\<le>R")
-  apply(drule Nat.le_imp_less_or_eq)
+  apply(drule le_imp_less_or_eq [of _ R])
   apply(erule disjE)
    apply(erule allE , erule (1) notE impE)
    apply force
diff -r cb3badaa192e -r 9e9e67e33557 src/HOL/HoareParallel/Mul_Gar_Coll.thy
--- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Tue Mar 18 20:33:29 2008 +0100
+++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Tue Mar 18 20:33:31 2008 +0100
@@ -383,7 +383,7 @@
 apply force
 --{* 1 subgoal left *}
 apply clarify
-apply(drule Nat.le_imp_less_or_eq)
+apply(drule_tac x = "ind x" in le_imp_less_or_eq)
 apply (simp_all add:Blacks_def)
 done
 
diff -r cb3badaa192e -r 9e9e67e33557 src/HOL/Hyperreal/Integration.thy
--- a/src/HOL/Hyperreal/Integration.thy	Tue Mar 18 20:33:29 2008 +0100
+++ b/src/HOL/Hyperreal/Integration.thy	Tue Mar 18 20:33:31 2008 +0100
@@ -561,7 +561,7 @@
 apply (frule partition_eq_bound)
 apply (drule_tac [2] partition_gt, auto)
 apply (metis dense_linear_order_class.dlo_simps(8) not_less partition_rhs partition_rhs2)
-apply (metis Nat.le_less_trans dense_linear_order_class.dlo_simps(8) nat_le_linear partition_eq_bound partition_rhs2)
+apply (metis le_less_trans dense_linear_order_class.dlo_simps(8) nat_le_linear partition_eq_bound partition_rhs2)
 done
 
 lemma lemma_additivity4_psize_eq:
@@ -574,7 +574,7 @@
 apply (auto intro: partition_lt_Suc)
 apply (drule_tac n = n in partition_lt_gen, assumption)
 apply (arith, arith)
-apply (cut_tac m = na and n = "psize D" in Nat.less_linear)
+apply (cut_tac x = na and y = "psize D" in less_linear)
 apply (auto dest: partition_lt_cancel)
 apply (rule_tac x=N and y=n in linorder_cases)
 apply (drule_tac x = n and P="%m. N \<le> m --> ?f m = ?g m" in spec, simp)
diff -r cb3badaa192e -r 9e9e67e33557 src/HOL/Hyperreal/Poly.thy
--- a/src/HOL/Hyperreal/Poly.thy	Tue Mar 18 20:33:29 2008 +0100
+++ b/src/HOL/Hyperreal/Poly.thy	Tue Mar 18 20:33:31 2008 +0100
@@ -739,7 +739,7 @@
       ==> EX! n. ([-a, 1] %^ n) divides p &
                  ~(([-a, 1] %^ (Suc n)) divides p)"
 apply (auto intro: poly_order_exists simp add: less_linear simp del: pmult_Cons pexp_Suc)
-apply (metis Suc_leI Nat.less_linear poly_exp_divides)
+apply (metis Suc_leI less_linear poly_exp_divides)
 done
 
 text{*Order*}
diff -r cb3badaa192e -r 9e9e67e33557 src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Tue Mar 18 20:33:29 2008 +0100
+++ b/src/HOL/Library/Permutation.thy	Tue Mar 18 20:33:31 2008 +0100
@@ -188,7 +188,7 @@
    apply (subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
     apply (fastsimp simp add: insert_ident)
    apply (metis distinct_remdups set_remdups)
-  apply (metis Nat.le_less_trans Suc_length_conv length_remdups_leq less_Suc_eq nat_less_le)
+  apply (metis le_less_trans Suc_length_conv length_remdups_leq less_Suc_eq nat_less_le)
   done
 
 lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y = (set x = set y)"
diff -r cb3badaa192e -r 9e9e67e33557 src/HOL/NumberTheory/Factorization.thy
--- a/src/HOL/NumberTheory/Factorization.thy	Tue Mar 18 20:33:29 2008 +0100
+++ b/src/HOL/NumberTheory/Factorization.thy	Tue Mar 18 20:33:31 2008 +0100
@@ -295,7 +295,7 @@
 lemma primel_prod_less:
   "primel (x # xs) ==>
     primel ys ==> prod (x # xs) = prod ys ==> prod xs < prod ys"
-  by (metis Nat.less_asym linorder_neqE_nat mult_less_cancel2 nat_0_less_mult_iff
+  by (metis less_asym linorder_neqE_nat mult_less_cancel2 nat_0_less_mult_iff
     nat_less_le nat_mult_1 prime_def primel_hd_tl primel_prod_gz prod.simps(2))
 
 lemma prod_one_empty: