# 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