# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1501072596 -3600
# Node ID 1ec601d9c829dc597d6924b489b1499a5b5a146f
# Parent  0442b3f4555682809ff7ef2dfa1ed75b950a9d59
moved transitive_stepwise_le into Nat, where it belongs

diff -r 0442b3f45556 -r 1ec601d9c829 src/HOL/Analysis/Tagged_Division.thy
--- a/src/HOL/Analysis/Tagged_Division.thy	Mon Jul 24 16:50:46 2017 +0100
+++ b/src/HOL/Analysis/Tagged_Division.thy	Wed Jul 26 13:36:36 2017 +0100
@@ -71,14 +71,6 @@
     by (simp add: field_simps)
 qed
 
-declare norm_triangle_ineq4[intro]
-
-lemma transitive_stepwise_le:
-  assumes "m \<le> n" "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" and "\<And>n. R n (Suc n)"
-  shows "R m n"
-using \<open>m \<le> n\<close>  
-  by (induction rule: dec_induct) (use assms in blast)+
-
 subsection \<open>Some useful lemmas about intervals.\<close>
 
 lemma interior_subset_union_intervals:
diff -r 0442b3f45556 -r 1ec601d9c829 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon Jul 24 16:50:46 2017 +0100
+++ b/src/HOL/Nat.thy	Wed Jul 26 13:36:36 2017 +0100
@@ -2143,6 +2143,12 @@
   qed
 qed
 
+lemma transitive_stepwise_le:
+  assumes "m \<le> n" "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" and "\<And>n. R n (Suc n)"
+  shows "R m n"
+using \<open>m \<le> n\<close>  
+  by (induction rule: dec_induct) (use assms in blast)+
+
 
 subsubsection \<open>Greatest operator\<close>