# HG changeset patch
# User blanchet
# Date 1384794285 -3600
# Node ID 478b4aa26a4c18819b1b726267c58a2d0909a1b0
# Parent  b4d644be252c4278b7304d20e4ee30f90c48a541
moved theorems out of LFP

diff -r b4d644be252c -r 478b4aa26a4c src/HOL/Cardinals/Constructions_on_Wellorders.thy
--- a/src/HOL/Cardinals/Constructions_on_Wellorders.thy	Mon Nov 18 18:04:45 2013 +0100
+++ b/src/HOL/Cardinals/Constructions_on_Wellorders.thy	Mon Nov 18 18:04:45 2013 +0100
@@ -13,8 +13,6 @@
 
 declare
   ordLeq_Well_order_simp[simp]
-  ordLess_Well_order_simp[simp]
-  ordIso_Well_order_simp[simp]
   not_ordLeq_iff_ordLess[simp]
   not_ordLess_iff_ordLeq[simp]
 
@@ -88,7 +86,7 @@
 by (auto simp add: ofilter_subset_embedS_iso)
 
 
-subsection {* Ordering the  well-orders by existence of embeddings *}
+subsection {* Ordering the well-orders by existence of embeddings *}
 
 corollary ordLeq_refl_on: "refl_on {r. Well_order r} ordLeq"
 using ordLeq_reflexive unfolding ordLeq_def refl_on_def
@@ -113,6 +111,16 @@
 corollary ordIso_equiv: "equiv {r. Well_order r} ordIso"
 by (auto simp add:  equiv_def ordIso_sym ordIso_refl_on ordIso_trans)
 
+lemma ordLess_Well_order_simp[simp]:
+assumes "r <o r'"
+shows "Well_order r \<and> Well_order r'"
+using assms unfolding ordLess_def by simp
+
+lemma ordIso_Well_order_simp[simp]:
+assumes "r =o r'"
+shows "Well_order r \<and> Well_order r'"
+using assms unfolding ordIso_def by simp
+
 lemma ordLess_irrefl: "irrefl ordLess"
 by(unfold irrefl_def, auto simp add: ordLess_irreflexive)
 
diff -r b4d644be252c -r 478b4aa26a4c src/HOL/Cardinals/Constructions_on_Wellorders_LFP.thy
--- a/src/HOL/Cardinals/Constructions_on_Wellorders_LFP.thy	Mon Nov 18 18:04:45 2013 +0100
+++ b/src/HOL/Cardinals/Constructions_on_Wellorders_LFP.thy	Mon Nov 18 18:04:45 2013 +0100
@@ -330,7 +330,7 @@
 
 
 
-subsection {* Ordering the  well-orders by existence of embeddings *}
+subsection {* Ordering the well-orders by existence of embeddings *}
 
 
 text {* We define three relations between well-orders:
@@ -383,18 +383,6 @@
 using assms unfolding ordLeq_def by simp
 
 
-lemma ordLess_Well_order_simp:
-assumes "r <o r'"
-shows "Well_order r \<and> Well_order r'"
-using assms unfolding ordLess_def by simp
-
-
-lemma ordIso_Well_order_simp:
-assumes "r =o r'"
-shows "Well_order r \<and> Well_order r'"
-using assms unfolding ordIso_def by simp
-
-
 text{* Notice that the relations @{text "\<le>o"}, @{text "<o"}, @{text "=o"} connect well-orders
 on potentially {\em distinct} types. However, some of the lemmas below, including the next one,
 restrict implicitly the type of these relations to @{text "(('a rel) * ('a rel)) set"} , i.e.,