author | kuncar |
Fri, 18 May 2012 17:36:20 +0200 | |
changeset 47943 | c09326cedb41 |
parent 47942 | 49b05b9ead33 |
child 47944 | e6b51fab96f7 |
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Fri May 18 16:43:38 2012 +0200 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Fri May 18 17:36:20 2012 +0200 @@ -211,6 +211,8 @@ |> pair NONE in lthy'' + |> (snd oo Local_Theory.note) ((Binding.prefix_name "Quotient_" qty_name, []), + [quot_thm]) |> (snd oo Local_Theory.note) ((qualify "bi_unique", [transfer_attr]), [[typedef_thm, T_def] MRSL @{thm typedef_bi_unique}]) |> (snd oo Local_Theory.note) ((qualify "rep_transfer", [transfer_attr]),