Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/UNITY/WFair.thy
changeset 14077 37c964462747
parent 12552 d2d2ab3f1f37
child 15634 bca33c49b083
equal deleted inserted replaced
14076:5cfc8b9fb880 14077:37c964462747 
    35     Trans  "[| <A,B> : leads(D, F); <B,C> : leads(D, F) |] ==>  <A,C>:leads(D, F)"
 
    35     Trans  "[| <A,B> : leads(D, F); <B,C> : leads(D, F) |] ==>  <A,C>:leads(D, F)"
 
    36     Union   "[| S:Pow({A:S. <A, B>:leads(D, F)}); B:Pow(D); S:Pow(Pow(D)) |] ==> 
    36     Union   "[| S:Pow({A:S. <A, B>:leads(D, F)}); B:Pow(D); S:Pow(Pow(D)) |] ==> 
    37 	      <Union(S),B>:leads(D, F)"
 
    37 	      <Union(S),B>:leads(D, F)"
 
    38 
    38 
    39   monos        Pow_mono
 
    39   monos        Pow_mono
 
    40   type_intrs  "[Union_PowI, UnionI, PowI]"
 
    40   type_intrs  "[Union_Pow_iff RS iffD2, UnionI, PowI]"
 
    41  
    41  
    42 constdefs
 
    42 constdefs
 
    43 
    43 
    44   (* The Visible version of the LEADS-TO relation*)
 
    44   (* The Visible version of the LEADS-TO relation*)
 
    45   leadsTo :: "[i, i] => i"       (infixl 60)
 
    45   leadsTo :: "[i, i] => i"       (infixl 60)
isabelle