equal
deleted
inserted
replaced
10 Ordered pairs and descriptions are defined using cons ("set notation") |
10 Ordered pairs and descriptions are defined using cons ("set notation") |
11 *) |
11 *) |
12 |
12 |
13 header{*Unordered Pairs*} |
13 header{*Unordered Pairs*} |
14 |
14 |
15 theory upair = ZF |
15 theory upair imports ZF |
16 files "Tools/typechk.ML": |
16 uses "Tools/typechk.ML" begin |
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))" |