equal
deleted
inserted
replaced
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 *) |
4 *) |
5 |
5 |
6 header {*Relativization and Absoluteness*} |
6 header {*Relativization and Absoluteness*} |
7 |
7 |
8 theory Relative = Main: |
8 theory Relative imports Main begin |
9 |
9 |
10 subsection{* Relativized versions of standard set-theoretic concepts *} |
10 subsection{* Relativized versions of standard set-theoretic concepts *} |
11 |
11 |
12 constdefs |
12 constdefs |
13 empty :: "[i=>o,i] => o" |
13 empty :: "[i=>o,i] => o" |