src/HOL/Matrix_LP/Matrix.thy
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