# HG changeset patch
# User berghofe
# Date 1210150762 -7200
# Node ID c0fa62fa0e5b07790d3870158150eb6a64434298
# Parent  067cceb36e2602f1e1a4719d8f2b115319b8a4de
Rephrased forward proofs to avoid problems with HO unification

diff -r 067cceb36e26 -r c0fa62fa0e5b src/HOL/Isar_examples/KnasterTarski.thy
--- a/src/HOL/Isar_examples/KnasterTarski.thy	Wed May 07 10:59:21 2008 +0200
+++ b/src/HOL/Isar_examples/KnasterTarski.thy	Wed May 07 10:59:22 2008 +0200
@@ -63,7 +63,7 @@
       finally (order_antisym) show ?thesis .
     }
     from mono ge have "f (f ?a) <= f ?a" ..
-    hence "f ?a : ?H" ..
+    hence "f ?a : ?H" by simp
     thus "?a <= f ?a" by (rule Inter_lower)
   qed
 qed
@@ -100,7 +100,7 @@
     show "?a <= f ?a"
     proof (rule Inter_lower)
       from mono ge have "f (f ?a) <= f ?a" ..
-      thus "f ?a : ?H" ..
+      thus "f ?a : ?H" by simp
     qed
   qed
 qed