| changeset 7253 | a494a78fea39 |
| parent 7153 | 820c8c8573d9 |
| child 7480 | 0a0e0dbe1269 |
--- a/src/HOL/Isar_examples/KnasterTarski.thy Wed Aug 18 16:04:00 1999 +0200 +++ b/src/HOL/Isar_examples/KnasterTarski.thy Wed Aug 18 16:05:27 1999 +0200 @@ -9,7 +9,6 @@ theory KnasterTarski = Main:; text {* - According to the book ``Introduction to Lattices and Order'' (by B. A. Davey and H. A. Priestley, CUP 1990), the Knaster-Tarski fixpoint theorem is as follows (pages 93--94). Note that we have