src/ZF/Constructible/Wellorderings.thy
changeset 13505 52a16cb7fefb
parent 13428 99e52e78eb65
child 13513 b9e14471629c
     1.1 --- a/src/ZF/Constructible/Wellorderings.thy	Fri Aug 16 12:48:49 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Fri Aug 16 16:41:48 2002 +0200
     1.3 @@ -1,3 +1,9 @@
     1.4 +(*  Title:      ZF/Constructible/Wellorderings.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   2002  University of Cambridge
     1.8 +*)
     1.9 +
    1.10  header {*Relativized Wellorderings*}
    1.11  
    1.12  theory Wellorderings = Relative:
    1.13 @@ -57,15 +63,15 @@
    1.14  
    1.15  lemma (in M_axioms) wellordered_is_trans_on: 
    1.16      "[| wellordered(M,A,r); M(A) |] ==> trans[A](r)"
    1.17 -by (auto simp add: wellordered_def )
    1.18 +by (auto simp add: wellordered_def)
    1.19  
    1.20  lemma (in M_axioms) wellordered_is_linear: 
    1.21      "[| wellordered(M,A,r); M(A) |] ==> linear(A,r)"
    1.22 -by (auto simp add: wellordered_def )
    1.23 +by (auto simp add: wellordered_def)
    1.24  
    1.25  lemma (in M_axioms) wellordered_is_wellfounded_on: 
    1.26      "[| wellordered(M,A,r); M(A) |] ==> wellfounded_on(M,A,r)"
    1.27 -by (auto simp add: wellordered_def )
    1.28 +by (auto simp add: wellordered_def)
    1.29  
    1.30  lemma (in M_axioms) wellfounded_imp_wellfounded_on: 
    1.31      "[| wellfounded(M,r); M(A) |] ==> wellfounded_on(M,A,r)"
    1.32 @@ -629,7 +635,7 @@
    1.33  lemma (in M_axioms) relativized_imp_well_ord: 
    1.34       "[| wellordered(M,A,r); M(A); M(r) |] ==> well_ord(A,r)" 
    1.35  apply (insert ordertype_exists [of A r], simp)
    1.36 -apply (blast intro: well_ord_ord_iso well_ord_Memrel )  
    1.37 +apply (blast intro: well_ord_ord_iso well_ord_Memrel)  
    1.38  done
    1.39  
    1.40  subsection {*Kunen's theorem 5.4, poage 127*}