summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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";