# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1443004567 -3600
# Node ID b033aeaab1b8a8372f40dc7e68f37e49e3efcebc
# Parent  37862ccec075817456845a0f7cf54f8f5d4557cf
fixed a VERY SLOW proof

diff -r 37862ccec075 -r b033aeaab1b8 src/HOL/MicroJava/DFA/Product.thy
--- a/src/HOL/MicroJava/DFA/Product.thy	Tue Sep 22 16:55:49 2015 +0100
+++ b/src/HOL/MicroJava/DFA/Product.thy	Wed Sep 23 11:36:07 2015 +0100
@@ -43,7 +43,7 @@
   "order(Product.le rA rB) = (order rA & order rB)"
 apply (unfold Semilat.order_def)
 apply simp
-apply blast
+apply meson
 done 
 
 lemma acc_le_prodI [intro!]: