# HG changeset patch
# User haftmann
# Date 1260539035 -3600
# Node ID eee04bbbae7e208fdb71c29d609d3d0ea8dff6ae
# Parent  b174d384293e9b77855a815b8cf7c022fb512be2
avoid dependency on implicit dest rule predicate1D in proofs

diff -r b174d384293e -r eee04bbbae7e src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Dec 09 12:26:42 2009 +0100
+++ b/src/HOL/List.thy	Fri Dec 11 14:43:55 2009 +0100
@@ -3463,7 +3463,7 @@
 inductive_cases listspE [elim!,noatp]: "listsp A (x # l)"
 
 lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
-by (rule predicate1I, erule listsp.induct, blast+)
+by (rule predicate1I, erule listsp.induct, (blast dest: predicate1D)+)
 
 lemmas lists_mono = listsp_mono [to_set pred_subset_eq]
 
diff -r b174d384293e -r eee04bbbae7e src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Dec 09 12:26:42 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Dec 11 14:43:55 2009 +0100
@@ -790,8 +790,11 @@
   unfolding hull_def using convex_Inter[of "{t\<in>convex. s\<subseteq>t}"]
   unfolding mem_def by auto
 
-lemma convex_hull_eq: "(convex hull s = s) \<longleftrightarrow> convex s" apply(rule hull_eq[unfolded mem_def])
-  using convex_Inter[unfolded Ball_def mem_def] by auto
+lemma convex_hull_eq: "convex hull s = s \<longleftrightarrow> convex s"
+  apply (rule hull_eq [unfolded mem_def])
+  apply (rule convex_Inter [unfolded Ball_def mem_def])
+  apply (simp add: le_fun_def le_bool_def)
+  done
 
 lemma bounded_convex_hull:
   fixes s :: "'a::real_normed_vector set"