--- a/src/HOL/MicroJava/BV/Product.thy Thu Nov 20 10:42:00 2003 +0100
+++ b/src/HOL/MicroJava/BV/Product.thy Fri Nov 21 11:15:40 2003 +0100
@@ -44,7 +44,7 @@
"order(Product.le rA rB) = (order rA & order rB)"
apply (unfold order_def)
apply simp
-apply blast
+apply meson
done