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 {*Absoluteness Properties for Recursive Datatypes*} |
6 header {*Absoluteness Properties for Recursive Datatypes*} |
7 |
7 |
8 theory Datatype_absolute = Formula + WF_absolute: |
8 theory Datatype_absolute imports Formula WF_absolute begin |
9 |
9 |
10 |
10 |
11 subsection{*The lfp of a continuous function can be expressed as a union*} |
11 subsection{*The lfp of a continuous function can be expressed as a union*} |
12 |
12 |
13 constdefs |
13 constdefs |