--- a/src/HOL/Library/Quickcheck_Types.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Library/Quickcheck_Types.thy Mon Sep 12 07:55:43 2011 +0200
@@ -353,7 +353,7 @@
}
from `x : A` this show "Inf A <= x"
unfolding Inf_flat_complete_lattice_def
- by fastsimp
+ by fastforce
next
fix z A
assume z: "\<And>x. x : A ==> z <= (x :: 'a flat_complete_lattice)"
@@ -412,7 +412,7 @@
}
from `x : A` this show "x <= Sup A"
unfolding Sup_flat_complete_lattice_def
- by fastsimp
+ by fastforce
next
fix z A
assume z: "\<And>x. x : A ==> x <= (z :: 'a flat_complete_lattice)"