src/HOL/Library/FSet.thy

 subsection \<open>Basic operations and type class instantiations\<close>
 
 (* FIXME transfer and right_total vs. bi_total *)
 instantiation fset :: (finite) finite
 begin
-instance by default (transfer, simp)
+instance by (standard; transfer; simp)
 end
 
 instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}"
 begin
 

 
 lift_definition minus_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is minus parametric Diff_transfer
   by simp
 
 instance
-by default (transfer, auto)+
+  by (standard; transfer; auto)+
 
 end
 
 abbreviation fempty :: "'a fset" ("{||}") where "{||} \<equiv> bot"
 abbreviation fsubset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subseteq>|" 50) where "xs |\<subseteq>| ys \<equiv> xs \<le> ys"

 end
 
 instantiation fset :: (finite) complete_lattice 
 begin
 
-lift_definition top_fset :: "'a fset" is UNIV parametric right_total_UNIV_transfer UNIV_transfer by simp
-
-instance by default (transfer, auto)+
+lift_definition top_fset :: "'a fset" is UNIV parametric right_total_UNIV_transfer UNIV_transfer
+  by simp
+
+instance
+  by (standard; transfer; auto)
+
 end
 
 instantiation fset :: (finite) complete_boolean_algebra
 begin
 
 lift_definition uminus_fset :: "'a fset \<Rightarrow> 'a fset" is uminus 
   parametric right_total_Compl_transfer Compl_transfer by simp
 
-instance by (default, simp_all only: INF_def SUP_def) (transfer, simp add: Compl_partition Diff_eq)+
+instance
+  by (standard, simp_all only: INF_def SUP_def) (transfer, simp add: Compl_partition Diff_eq)+
 
 end
 
 abbreviation fUNIV :: "'a::finite fset" where "fUNIV \<equiv> top"
 abbreviation fuminus :: "'a::finite fset \<Rightarrow> 'a fset" ("|-| _" [81] 80) where "|-| x \<equiv> uminus x"