src/HOL/Quotient_Examples/Lift_Set.thy

 
 definition set where "set = (UNIV :: ('a \<Rightarrow> bool) set)"
 
 typedef 'a set = "set :: ('a \<Rightarrow> bool) set"
   morphisms member Set
-  unfolding set_def by auto
+  unfolding set_def by (rule UNIV_witness)
 
 setup_lifting type_definition_set[unfolded set_def]
 
 text {* Now, we can employ lift_definition to lift definitions. *}
 
-lift_definition empty :: "'a set" is "bot :: 'a \<Rightarrow> bool" done
+lift_definition empty :: "'a set" is "bot :: 'a \<Rightarrow> bool" .
 
 term "Lift_Set.empty"
 thm Lift_Set.empty_def
 
-lift_definition insert :: "'a => 'a set => 'a set" is "\<lambda> x P y. y = x \<or> P y" done 
+lift_definition insert :: "'a => 'a set => 'a set" is "\<lambda> x P y. y = x \<or> P y" . 
 
 term "Lift_Set.insert"
 thm Lift_Set.insert_def
 
 export_code empty insert in SML
 
 end
-