summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sat, 03 Jul 1999 00:28:05 +0200 | |

changeset 6893 | 6e56603fb339 |

parent 6892 | 4a905b4a39c8 |

child 6894 | b92c2f0413b8 |

proper text;

--- a/src/HOL/Isar_examples/KnasterTarski.thy Sat Jul 03 00:26:00 1999 +0200 +++ b/src/HOL/Isar_examples/KnasterTarski.thy Sat Jul 03 00:28:05 1999 +0200 @@ -11,7 +11,7 @@ theorems [dest] = monoD; (* FIXME [dest!!] *) -(* +text {* The proof of Knaster-Tarski below closely follows the presentation in 'Introduction to Lattices' and Order by Davey/Priestley, pages 93--94. All of their narration has been rephrased in terms of formal @@ -22,7 +22,7 @@ Just as many textbook-style proofs, there is a strong bias towards forward reasoning, with little hierarchical structure. -*) +*}; theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a"; proof;