# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259585885 -3600
# Node ID 40c9fb60de3cfed4fd4d0f4bf879115bf038b542
# Parent  3f8c7183ddacdf8d3435e2da8e0a1a6c78d95ddc# Parent  020e27417b59882e38630a8cdf77f0f685f369e8
merged

diff -r 020e27417b59 -r 40c9fb60de3c QuotMain.thy
--- a/QuotMain.thy	Mon Nov 30 12:14:20 2009 +0100
+++ b/QuotMain.thy	Mon Nov 30 13:58:05 2009 +0100
@@ -1236,6 +1236,9 @@
     end) lthy
 *}
 
+thm EQUIV_REFL
+thm equiv_trans2
+
 ML {*
 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *)
 fun lift_tac lthy rthm rel_eqv rty quot defs =
diff -r 020e27417b59 -r 40c9fb60de3c quotient_info.ML
--- a/quotient_info.ML	Mon Nov 30 12:14:20 2009 +0100
+++ b/quotient_info.ML	Mon Nov 30 13:58:05 2009 +0100
@@ -11,6 +11,7 @@
   val quotdata_lookup: Proof.context -> string -> quotient_info option
   val quotdata_update_thy: string -> (typ * typ * term * thm) -> theory -> theory
   val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context
+  val quotdata_dest: theory -> quotient_info list
 
   type qconsts_info = {qconst: term, rconst: term}
   val qconsts_transfer: morphism -> qconsts_info -> qconsts_info
@@ -88,6 +89,9 @@
 fun quotdata_update qty_name (qty, rty, rel, equiv_thm) = 
       ProofContext.theory (quotdata_update_thy qty_name (qty, rty, rel, equiv_thm))
 
+fun quotdata_dest thy =
+    map snd (Symtab.dest (QuotData.get thy))
+
 fun print_quotinfo ctxt =
 let
   fun prt_quot {qtyp, rtyp, rel, equiv_thm} =