changeset 74334 | ead56ad40e15 |
parent 71925 | bf085daea304 |
child 76987 | 4c275405faae |
74333:a9b20bc32fa6 | 74334:ead56ad40e15 |
---|---|
5 *) |
5 *) |
6 |
6 |
7 section \<open>Textbook-style reasoning: the Knaster-Tarski Theorem\<close> |
7 section \<open>Textbook-style reasoning: the Knaster-Tarski Theorem\<close> |
8 |
8 |
9 theory Knaster_Tarski |
9 theory Knaster_Tarski |
10 imports Main "HOL-Library.Lattice_Syntax" |
10 imports Main |
11 begin |
11 begin |
12 |
|
13 unbundle lattice_syntax |
|
12 |
14 |
13 |
15 |
14 subsection \<open>Prose version\<close> |
16 subsection \<open>Prose version\<close> |
15 |
17 |
16 text \<open> |
18 text \<open> |