src/ZF/Integ/Int.ML

--- a/src/ZF/Integ/Int.ML	Thu Jul 13 23:26:08 2000 +0200
+++ b/src/ZF/Integ/Int.ML	Fri Jul 14 13:39:03 2000 +0200
@@ -105,6 +105,8 @@
 by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
 qed "zminus_congruent";
 
+val RSLIST = curry (op MRS);
+
 (*Resolve th against the corresponding facts for zminus*)
 val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];