--- a/src/Pure/drule.ML Tue Feb 14 20:43:32 2012 +0100
+++ b/src/Pure/drule.ML Tue Feb 14 20:57:05 2012 +0100
@@ -4,7 +4,7 @@
Derived rules and other operations on theorems.
*)
-infix 0 RS RSN RL RLN MRS MRL OF COMP INCR_COMP COMP_INCR;
+infix 0 RS RSN RL RLN MRS OF COMP INCR_COMP COMP_INCR;
signature BASIC_DRULE =
sig
@@ -35,7 +35,6 @@
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
val compose: thm * int * thm -> thm list
val COMP: thm * thm -> thm
@@ -390,12 +389,6 @@
| rs_aux i (rl::rls) = rl RSN (i, rs_aux (i+1) rls)
in rs_aux 1 rls end;
-(*As above, but for rule lists*)
-fun rlss MRL bottom_rls =
- let fun rs_aux i [] = bottom_rls
- | rs_aux i (rls::rlss) = rls RLN (i, rs_aux (i+1) rlss)
- in rs_aux 1 rlss end;
-
(*A version of MRS with more appropriate argument order*)
fun bottom_rl OF rls = rls MRS bottom_rl;