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