src/HOL/Library/FSet.thy
changeset 62343 24106dc44def
parent 62324 ae44f16dcea5
child 62390 842917225d56
--- a/src/HOL/Library/FSet.thy	Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Library/FSet.thy	Wed Feb 17 21:51:56 2016 +0100
@@ -147,7 +147,7 @@
   parametric right_total_Compl_transfer Compl_transfer by simp
 
 instance
-  by (standard, simp_all only: INF_def SUP_def) (transfer, simp add: Compl_partition Diff_eq)+
+  by (standard; transfer) (simp_all add: Diff_eq)
 
 end