src/ZF/upair.thy
changeset 15091 77d160469390
parent 14883 ca000a495448
child 16417 9bc16273c2d4
equal deleted inserted replaced
15090:970c2668c694 15091:77d160469390
    11 *)
    11 *)
    12 
    12 
    13 header{*Unordered Pairs*}
    13 header{*Unordered Pairs*}
    14 
    14 
    15 theory upair = ZF
    15 theory upair = ZF
    16 files "Tools/typechk":
    16 files "Tools/typechk.ML":
    17 
    17 
    18 setup TypeCheck.setup
    18 setup TypeCheck.setup
    19 
    19 
    20 lemma atomize_ball [symmetric, rulify]:
    20 lemma atomize_ball [symmetric, rulify]:
    21      "(!!x. x:A ==> P(x)) == Trueprop (ALL x:A. P(x))"
    21      "(!!x. x:A ==> P(x)) == Trueprop (ALL x:A. P(x))"