--- a/src/HOL/Quotient_Examples/Lift_Set.thy Fri Mar 23 14:25:31 2012 +0100
+++ b/src/HOL/Quotient_Examples/Lift_Set.thy Fri Mar 23 14:26:09 2012 +0100
@@ -14,25 +14,7 @@
morphisms member Set
unfolding set_def by auto
-text {* Here is some ML setup that should eventually be incorporated in the typedef command. *}
-
-local_setup {* fn lthy =>
- let
- val quotients =
- {qtyp = @{typ "'a set"}, rtyp = @{typ "'a => bool"},
- equiv_rel = @{term "op ="}, equiv_thm = @{thm refl}}
- val qty_full_name = @{type_name "set"}
-
- fun qinfo phi = Quotient_Info.transform_quotients phi quotients
- in
- lthy
- |> Local_Theory.declaration {syntax = false, pervasive = true}
- (fn phi =>
- Quotient_Info.update_quotients qty_full_name (qinfo phi) #>
- Quotient_Info.update_abs_rep qty_full_name
- (Quotient_Info.transform_abs_rep phi {abs = @{term "Set"}, rep = @{term "member"}}))
- end
-*}
+setup_lifting type_definition_set[unfolded set_def]
text {* Now, we can employ quotient_definition to lift definitions. *}
@@ -51,5 +33,7 @@
term "Lift_Set.insert"
thm Lift_Set.insert_def
+export_code empty insert in SML
+
end