# HG changeset patch # User wenzelm # Date 931539541 -7200 # Node ID d8026ebe4516e529ede5eae0e5768b749b8ba1a3 # Parent 18c0457efd3d74c572d818828a2c1d1bbf8abf04 mono: extra I/E; diff -r 18c0457efd3d -r d8026ebe4516 src/HOL/Isar_examples/KnasterTarski.thy --- a/src/HOL/Isar_examples/KnasterTarski.thy Fri Jul 09 18:58:05 1999 +0200 +++ b/src/HOL/Isar_examples/KnasterTarski.thy Fri Jul 09 18:59:01 1999 +0200 @@ -9,8 +9,6 @@ theory KnasterTarski = Main:; -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