src/ZF/Integ/Int.ML
changeset 9333 5cacc383157a
parent 8201 a81d18b0a9b1
child 9491 1a36151ee2fc
     1.1 --- a/src/ZF/Integ/Int.ML	Thu Jul 13 23:26:08 2000 +0200
     1.2 +++ b/src/ZF/Integ/Int.ML	Fri Jul 14 13:39:03 2000 +0200
     1.3 @@ -105,6 +105,8 @@
     1.4  by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
     1.5  qed "zminus_congruent";
     1.6  
     1.7 +val RSLIST = curry (op MRS);
     1.8 +
     1.9  (*Resolve th against the corresponding facts for zminus*)
    1.10  val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
    1.11