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