src/ZF/Constructible/Wellorderings.thy
changeset 16417 9bc16273c2d4
parent 13780 af7b79271364
child 21233 5a5c8ea5f66a
equal deleted inserted replaced
16416:6061ae1f90f2 16417:9bc16273c2d4
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4 *)
     4 *)
     5 
     5 
     6 header {*Relativized Wellorderings*}
     6 header {*Relativized Wellorderings*}
     7 
     7 
     8 theory Wellorderings = Relative:
     8 theory Wellorderings imports Relative begin
     9 
     9 
    10 text{*We define functions analogous to @{term ordermap} @{term ordertype} 
    10 text{*We define functions analogous to @{term ordermap} @{term ordertype} 
    11       but without using recursion.  Instead, there is a direct appeal
    11       but without using recursion.  Instead, there is a direct appeal
    12       to Replacement.  This will be the basis for a version relativized
    12       to Replacement.  This will be the basis for a version relativized
    13       to some class @{text M}.  The main result is Theorem I 7.6 in Kunen,
    13       to some class @{text M}.  The main result is Theorem I 7.6 in Kunen,