diff -r 9cb45d022524 -r 3f8c7183ddac QuotMain.thy
--- 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 =