src/Pure/drule.ML
changeset 13606 2f121149acfe
parent 13569 69a6b3aa0f38
child 13650 31bd2a8cdbe2
     1.1 --- a/src/Pure/drule.ML	Mon Sep 30 16:36:57 2002 +0200
     1.2 +++ b/src/Pure/drule.ML	Mon Sep 30 16:37:44 2002 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  Derived rules and other operations on theorems.
     1.5  *)
     1.6  
     1.7 -infix 0 RS nRS RSN RL RLN MRS MRL OF COMP;
     1.8 +infix 0 RS RSN RL RLN MRS MRL OF COMP;
     1.9  
    1.10  signature BASIC_DRULE =
    1.11  sig
    1.12 @@ -45,7 +45,6 @@
    1.13    val assume_ax         : theory -> string -> thm
    1.14    val RSN               : thm * (int * thm) -> thm
    1.15    val RS                : thm * thm -> thm
    1.16 -  val nRS               : thm * thm -> thm
    1.17    val RLN               : thm list * (int * thm list) -> thm list
    1.18    val RL                : thm list * thm list -> thm list
    1.19    val MRS               : thm list * thm -> thm
    1.20 @@ -458,10 +457,6 @@
    1.21  (*resolution: P==>Q, Q==>R gives P==>R. *)
    1.22  fun tha RS thb = tha RSN (1,thb);
    1.23  
    1.24 -(* preserves the name of the thm on the LEFT: *)
    1.25 -fun th nRS rl = Thm.name_thm (Thm.name_of_thm th, th RS rl)
    1.26 -
    1.27 -
    1.28  (*For joining lists of rules*)
    1.29  fun thas RLN (i,thbs) =
    1.30    let val resolve = biresolution false (map (pair false) thas) i