equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 section \<open>The Full Theorem of Tarski\<close> |
5 section \<open>The Full Theorem of Tarski\<close> |
6 |
6 |
7 theory Tarski |
7 theory Tarski |
8 imports Main HOL.FuncSet |
8 imports Main "HOL-Library.FuncSet" |
9 begin |
9 begin |
10 |
10 |
11 text \<open> |
11 text \<open> |
12 Minimal version of lattice theory plus the full theorem of Tarski: |
12 Minimal version of lattice theory plus the full theorem of Tarski: |
13 The fixedpoints of a complete lattice themselves form a complete |
13 The fixedpoints of a complete lattice themselves form a complete |