--- a/src/HOL/Quotient_Examples/Lift_Set.thy Wed Feb 19 22:02:23 2014 +1100
+++ b/src/HOL/Quotient_Examples/Lift_Set.thy Wed Feb 19 16:32:37 2014 +0100
@@ -12,18 +12,18 @@
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
@@ -31,4 +31,3 @@
export_code empty insert in SML
end
-