equal
deleted
inserted
replaced
1 (* Title: ZF/Constructible/Datatype_absolute.thy |
1 (* Title: ZF/Constructible/Datatype_absolute.thy |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 *) |
3 *) |
4 |
4 |
5 header {*Absoluteness Properties for Recursive Datatypes*} |
5 section {*Absoluteness Properties for Recursive Datatypes*} |
6 |
6 |
7 theory Datatype_absolute imports Formula WF_absolute begin |
7 theory Datatype_absolute imports Formula WF_absolute begin |
8 |
8 |
9 |
9 |
10 subsection{*The lfp of a continuous function can be expressed as a union*} |
10 subsection{*The lfp of a continuous function can be expressed as a union*} |