src/Pure/drule.ML
changeset 9288 06a55195741b
parent 8605 625fbbe5c6b4
child 9418 96973ec6fda4
     1.1 --- a/src/Pure/drule.ML	Wed Jul 12 14:47:55 2000 +0200
     1.2 +++ b/src/Pure/drule.ML	Wed Jul 12 16:44:34 2000 +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 RSN RL RLN MRS MRL 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 @@ -42,6 +42,7 @@
    1.13    val RL                : thm list * thm list -> thm list
    1.14    val MRS               : thm list * thm -> thm
    1.15    val MRL               : thm list list * thm list -> thm list
    1.16 +  val OF                : thm * thm list -> thm
    1.17    val compose           : thm * int * thm -> thm list
    1.18    val COMP              : thm * thm -> thm
    1.19    val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm
    1.20 @@ -349,6 +350,9 @@
    1.21          | rs_aux i (rls::rlss) = rls RLN (i, rs_aux (i+1) rlss)
    1.22    in  rs_aux 1 rlss  end;
    1.23  
    1.24 +(*A version of MRS with more appropriate argument order*)
    1.25 +fun bottom_rl OF rls = rls MRS bottom_rl;
    1.26 +
    1.27  (*compose Q and [...,Qi,Q(i+1),...]==>R to [...,Q(i+1),...]==>R
    1.28    with no lifting or renaming!  Q may contain ==> or meta-quants
    1.29    ALWAYS deletes premise i *)