# HG changeset patch
# User ballarin
# Date 1190134337 -7200
# Node ID 85a6c200ecd39d6cee3f73eeb170bc3868c29c88
# Parent  9b73bc9b05a1718a4cc45375c6fc7ba3342f68fd
Simplified proofs due to transitivity reasoner setup.

diff -r 9b73bc9b05a1 -r 85a6c200ecd3 src/HOL/Dense_Linear_Order.thy
--- a/src/HOL/Dense_Linear_Order.thy	Tue Sep 18 18:51:07 2007 +0200
+++ b/src/HOL/Dense_Linear_Order.thy	Tue Sep 18 18:52:17 2007 +0200
@@ -232,15 +232,8 @@
   from fU neU have th2: "?MU \<in> U" and th2': "\<forall>u\<in>U. ?MU \<sqsubseteq> u" by auto
   from th1 th2 H have "?ML \<sqsubset> ?MU" by auto
   with dense obtain w where th3: "?ML \<sqsubset> w" and th4: "w \<sqsubset> ?MU" by blast
-  from th3 th1' have "\<forall>l \<in> L. l \<sqsubset> w" 
-    apply auto
-    apply (erule_tac x="l" in ballE)
-    by (auto intro: le_less_trans)
-
-  moreover from th4 th2' have "\<forall>u \<in> U. w \<sqsubset> u" 
-    apply auto
-    apply (erule_tac x="u" in ballE)
-    by (auto intro: less_le_trans)
+  from th3 th1' have "\<forall>l \<in> L. l \<sqsubset> w" by auto
+  moreover from th4 th2' have "\<forall>u \<in> U. w \<sqsubset> u" by auto
   ultimately show "\<exists>x. (\<forall>y\<in>L. y \<^loc>< x) \<and> (\<forall>y\<in>U. x \<^loc>< y)" by auto
 qed
 
diff -r 9b73bc9b05a1 -r 85a6c200ecd3 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Tue Sep 18 18:51:07 2007 +0200
+++ b/src/HOL/Lattices.thy	Tue Sep 18 18:52:17 2007 +0200
@@ -289,8 +289,7 @@
   fix x y z
   show "max x (min y z) = min (max x y) (max x z)"
   unfolding min_def max_def
-    by (auto simp add: intro: antisym, unfold not_le,
-      auto intro: less_trans le_less_trans aux)
+  by auto
 qed (auto simp add: min_def max_def not_le less_imp_le)
 
 interpretation min_max:
diff -r 9b73bc9b05a1 -r 85a6c200ecd3 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Sep 18 18:51:07 2007 +0200
+++ b/src/HOL/List.thy	Tue Sep 18 18:52:17 2007 +0200
@@ -2509,7 +2509,6 @@
 lemma sorted_insort: "sorted (insort x xs) = sorted xs"
 apply (induct xs)
  apply(auto simp:sorted_Cons set_insort not_le less_imp_le)
-apply(blast intro:order_trans)
 done
 
 theorem sorted_sort[simp]: "sorted (sort xs)"