equal
deleted
inserted
replaced
89 Higher-Order Logic |
89 Higher-Order Logic |
90 |
90 |
91 page 243: Pow is a new constant of type 'a set => 'a set set |
91 page 243: Pow is a new constant of type 'a set => 'a set set |
92 |
92 |
93 page 246: Pow is defined by Pow(A) == {B. B <= A} |
93 page 246: Pow is defined by Pow(A) == {B. B <= A} |
|
94 empty_def should be {} == {x.False} |
94 |
95 |
95 page 248: Pow has the rules |
96 page 248: Pow has the rules |
96 PowI A<=B ==> A: Pow(B) |
97 PowI A<=B ==> A: Pow(B) |
97 PowD A: Pow(B) ==> A<=B |
98 PowD A: Pow(B) ==> A<=B |
98 |
99 |