# HG changeset patch
# User hoelzl
# Date 1436284890 -7200
# Node ID 9ce7463350a90adf515a369aa86234f646800889
# Parent  589ed01b94fe333a968e41e80a50304cb19fdc3f
add monotonicity rule for rtranclp

diff -r 589ed01b94fe -r 9ce7463350a9 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Tue Jul 07 00:48:42 2015 +0200
+++ b/src/HOL/Transitive_Closure.thy	Tue Jul 07 18:01:30 2015 +0200
@@ -104,6 +104,10 @@
    apply (rule_tac [2] rtranclp.rtrancl_into_rtrancl, blast+)
   done
 
+lemma mono_rtranclp[mono]:
+   "(\<And>a b. x a b \<longrightarrow> y a b) \<Longrightarrow> x^** a b \<longrightarrow> y^** a b"
+   using rtranclp_mono[of x y] by auto
+
 lemmas rtrancl_mono = rtranclp_mono [to_set]
 
 theorem rtranclp_induct [consumes 1, case_names base step, induct set: rtranclp]: