src/ZF/Constructible/Wellorderings.thy
changeset 21233 5a5c8ea5f66a
parent 16417 9bc16273c2d4
child 21404 eb85850d3eb7
equal deleted inserted replaced
21232:faacfd4392b5 21233:5a5c8ea5f66a
    14       page 17.*}
    14       page 17.*}
    15 
    15 
    16 
    16 
    17 subsection{*Wellorderings*}
    17 subsection{*Wellorderings*}
    18 
    18 
    19 constdefs
    19 definition
    20   irreflexive :: "[i=>o,i,i]=>o"
    20   irreflexive :: "[i=>o,i,i]=>o"
    21     "irreflexive(M,A,r) == \<forall>x[M]. x\<in>A --> <x,x> \<notin> r"
    21     "irreflexive(M,A,r) == \<forall>x[M]. x\<in>A --> <x,x> \<notin> r"
    22   
    22   
    23   transitive_rel :: "[i=>o,i,i]=>o"
    23   transitive_rel :: "[i=>o,i,i]=>o"
    24     "transitive_rel(M,A,r) == 
    24     "transitive_rel(M,A,r) ==