src/HOL/Isar_examples/KnasterTarski.thy
 changeset 7982 d534b897ce39 parent 7874 180364256231 child 8902 a705822f4e2a
```     1.1 --- a/src/HOL/Isar_examples/KnasterTarski.thy	Sat Oct 30 20:13:16 1999 +0200
1.2 +++ b/src/HOL/Isar_examples/KnasterTarski.thy	Sat Oct 30 20:20:48 1999 +0200
1.3 @@ -37,7 +37,8 @@
1.4   The Isar proof below closely follows the original presentation.
1.5   Virtually all of the prose narration has been rephrased in terms of
1.6   formal Isar language elements.  Just as many textbook-style proofs,
1.7 - there is a strong bias towards forward reasoning.
1.8 + there is a strong bias towards forward proof, and several bends
1.9 + in the course of reasoning.
1.10  *};
1.11
1.12  theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a";
1.13 @@ -72,11 +73,11 @@
1.14   explicit block structure and weak assumptions.  Thus we have mimicked
1.15   the particular way of reasoning of the original text.
1.16
1.17 - In the subsequent version of the proof the order of reasoning is
1.18 - changed to achieve structured top-down decomposition of the problem
1.19 - at the outer level, while the small inner steps of reasoning or done
1.20 - in a forward manner.  Note that this requires only the most basic
1.21 - features of the Isar language, we are certainly more at ease here.
1.22 + In the subsequent version the order of reasoning is changed to
1.23 + achieve structured top-down decomposition of the problem at the outer
1.24 + level, while only the inner steps of reasoning are done in a forward
1.25 + manner.  We are certainly more at ease here, requiring only the most
1.26 + basic features of the Isar language.
1.27  *};
1.28
1.29  theorem KnasterTarski': "mono f ==> EX a::'a set. f a = a";
```