src/Pure/drule.ML

     Copyright   1993  University of Cambridge
 
 Derived rules and other operations on theorems.
 *)
 
-infix 0 RS nRS RSN RL RLN MRS MRL OF COMP;
+infix 0 RS RSN RL RLN MRS MRL OF COMP;
 
 signature BASIC_DRULE =
 sig
   val mk_implies        : cterm * cterm -> cterm
   val list_implies      : cterm list * cterm -> cterm

   val rotate_prems      : int -> thm -> thm
   val rearrange_prems   : int list -> thm -> thm
   val assume_ax         : theory -> string -> thm
   val RSN               : thm * (int * thm) -> thm
   val RS                : thm * thm -> thm
-  val nRS               : thm * thm -> thm
   val RLN               : thm list * (int * thm list) -> thm list
   val RL                : thm list * thm list -> thm list
   val MRS               : thm list * thm -> thm
   val MRL               : thm list list * thm list -> thm list
   val OF                : thm * thm list -> thm

     |      _   => raise THM("RSN: multiple unifiers", i, [tha,thb]);
 
 (*resolution: P==>Q, Q==>R gives P==>R. *)
 fun tha RS thb = tha RSN (1,thb);
 
-(* preserves the name of the thm on the LEFT: *)
-fun th nRS rl = Thm.name_thm (Thm.name_of_thm th, th RS rl)
-
-
 (*For joining lists of rules*)
 fun thas RLN (i,thbs) =
   let val resolve = biresolution false (map (pair false) thas) i
       fun resb thb = Seq.list_of (resolve thb) handle THM _ => []
   in  List.concat (map resb thbs)  end;