Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Lifting/lifting_setup.ML
changeset 47943 c09326cedb41
parent 47937 70375fa2679d
child 47951 8c8a03765de7 
--- 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]),
isabelle