changeset 61236 | b033aeaab1b8 |
parent 58886 | 8a6cac7c7247 |
child 61361 | 8b5f00202e1a |
--- 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!]: