# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259591586 -3600
# Node ID 871fce48087fc861a7f1101e4605b16a1b3ec946
# Parent  0911d3aabf471e4d82938c979893ef2558c6dda5# Parent  40c9fb60de3cfed4fd4d0f4bf879115bf038b542
merge

diff -r 0911d3aabf47 -r 871fce48087f QuotMain.thy
--- a/QuotMain.thy	Mon Nov 30 15:32:14 2009 +0100
+++ b/QuotMain.thy	Mon Nov 30 15:33:06 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 0911d3aabf47 -r 871fce48087f quotient_info.ML
--- a/quotient_info.ML	Mon Nov 30 15:32:14 2009 +0100
+++ b/quotient_info.ML	Mon Nov 30 15:33:06 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} =