--- a/QuotMain.thy	Sun Nov 29 23:59:37 2009 +0100
+++ b/QuotMain.thy	Mon Nov 30 12:26:08 2009 +0100
@@ -1217,6 +1217,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 =