src/ZF/Constructible/Wellorderings.thy
changeset 13505 52a16cb7fefb
parent 13428 99e52e78eb65
child 13513 b9e14471629c
--- a/src/ZF/Constructible/Wellorderings.thy	Fri Aug 16 12:48:49 2002 +0200
+++ b/src/ZF/Constructible/Wellorderings.thy	Fri Aug 16 16:41:48 2002 +0200
@@ -1,3 +1,9 @@
+(*  Title:      ZF/Constructible/Wellorderings.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2002  University of Cambridge
+*)
+
 header {*Relativized Wellorderings*}
 
 theory Wellorderings = Relative:
@@ -57,15 +63,15 @@
 
 lemma (in M_axioms) wellordered_is_trans_on: 
     "[| wellordered(M,A,r); M(A) |] ==> trans[A](r)"
-by (auto simp add: wellordered_def )
+by (auto simp add: wellordered_def)
 
 lemma (in M_axioms) wellordered_is_linear: 
     "[| wellordered(M,A,r); M(A) |] ==> linear(A,r)"
-by (auto simp add: wellordered_def )
+by (auto simp add: wellordered_def)
 
 lemma (in M_axioms) wellordered_is_wellfounded_on: 
     "[| wellordered(M,A,r); M(A) |] ==> wellfounded_on(M,A,r)"
-by (auto simp add: wellordered_def )
+by (auto simp add: wellordered_def)
 
 lemma (in M_axioms) wellfounded_imp_wellfounded_on: 
     "[| wellfounded(M,r); M(A) |] ==> wellfounded_on(M,A,r)"
@@ -629,7 +635,7 @@
 lemma (in M_axioms) relativized_imp_well_ord: 
      "[| wellordered(M,A,r); M(A); M(r) |] ==> well_ord(A,r)" 
 apply (insert ordertype_exists [of A r], simp)
-apply (blast intro: well_ord_ord_iso well_ord_Memrel )  
+apply (blast intro: well_ord_ord_iso well_ord_Memrel)  
 done
 
 subsection {*Kunen's theorem 5.4, poage 127*}