author kuncar Tue, 17 Apr 2012 09:12:15 +0200 changeset 47502 4c949049cd78 parent 47501 0b9294e093db child 47503 cb44d09d9d22
note the Quotient theorem in quotient_type
```--- a/src/HOL/Tools/Quotient/quotient_type.ML	Mon Apr 16 20:50:43 2012 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Tue Apr 17 09:12:15 2012 +0200
@@ -136,6 +136,9 @@
let
val (_ \$ _ \$ abs_fun \$ _) = (HOLogic.dest_Trueprop o prop_of) quot3_thm
val (T_def, lthy') = define_cr_rel equiv_thm abs_fun lthy
+    val (rty, qty) = (dest_funT o fastype_of) abs_fun
+    val qty_name = (fst o dest_Type) qty
+    val quotient_thm_name = Binding.prefix_name "Quotient_" (Binding.qualified_name qty_name)
val quot_thm = (case (HOLogic.dest_Trueprop o prop_of) equiv_thm of
Const (@{const_name equivp}, _) \$ _ =>
[quot3_thm, T_def, equiv_thm] MRSL @{thm Quotient3_to_Quotient_equivp}
@@ -144,7 +147,9 @@
| _ => error "unsupported equivalence theorem"
)
in
-    Lifting_Setup.setup_lifting_infr quot_thm equiv_thm lthy'
+    lthy'
+      |> Lifting_Setup.setup_lifting_infr quot_thm equiv_thm
+      |> (snd oo Local_Theory.note) ((quotient_thm_name, []), [quot_thm])
end

fun init_quotient_infr quot_thm equiv_thm lthy =```