changeset 32960 | 69916a850301 |
parent 21404 | eb85850d3eb7 |
child 46823 | 57bf0cecb366 |
32959:23a8c5ac35f8 | 32960:69916a850301 |
---|---|
1 (* Title: ZF/Constructible/DPow_absolute.thy |
1 (* Title: ZF/Constructible/DPow_absolute.thy |
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 *) |
3 *) |
5 |
4 |
6 header {*Absoluteness for the Definable Powerset Function*} |
5 header {*Absoluteness for the Definable Powerset Function*} |
7 |
6 |