note Quotient theorem for typedefs in setup_lifting
authorkuncar
Fri May 18 17:36:20 2012 +0200 (2012-05-18)
changeset 47943c09326cedb41
parent 47942 49b05b9ead33
child 47944 e6b51fab96f7
note Quotient theorem for typedefs in setup_lifting
src/HOL/Tools/Lifting/lifting_setup.ML
     1.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Fri May 18 16:43:38 2012 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Fri May 18 17:36:20 2012 +0200
     1.3 @@ -211,6 +211,8 @@
     1.4          |> pair NONE
     1.5    in
     1.6      lthy''
     1.7 +      |> (snd oo Local_Theory.note) ((Binding.prefix_name "Quotient_" qty_name, []), 
     1.8 +        [quot_thm])
     1.9        |> (snd oo Local_Theory.note) ((qualify "bi_unique", [transfer_attr]), 
    1.10          [[typedef_thm, T_def] MRSL @{thm typedef_bi_unique}])
    1.11        |> (snd oo Local_Theory.note) ((qualify "rep_transfer", [transfer_attr]),