--- 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 =