changeset 61169 | 4de9ff3ea29a |
parent 61076 | bdc1e2f0a86a |
child 61260 | e6f03fae14d5 |
--- a/src/HOL/Matrix_LP/Matrix.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Matrix_LP/Matrix.thy Sun Sep 13 22:56:52 2015 +0200 @@ -1448,7 +1448,7 @@ definition "sup = combine_matrix sup" instance - by default (auto simp add: le_infI le_matrix_def inf_matrix_def sup_matrix_def) + by standard (auto simp add: le_infI le_matrix_def inf_matrix_def sup_matrix_def) end