src/HOL/Orderings.thy
changeset 59000 6eb0725503fc
parent 58893 9e0ecb66d6a7
child 59582 0fbed69ff081
     1.1 --- a/src/HOL/Orderings.thy	Thu Nov 13 14:40:06 2014 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Thu Nov 13 17:19:52 2014 +0100
     1.3 @@ -1524,6 +1524,9 @@
     1.4  lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x"
     1.5    by (rule le_funE)
     1.6  
     1.7 +lemma mono_compose: "mono Q \<Longrightarrow> mono (\<lambda>i x. Q i (f x))"
     1.8 +  unfolding mono_def le_fun_def by auto
     1.9 +
    1.10  
    1.11  subsection {* Order on unary and binary predicates *}
    1.12