src/ZF/ROOT.ML
changeset 14 1c0926788772
parent 6 8ce8c4d13d4d
child 32 a8f1cdbbc5b8
     1.1 --- a/src/ZF/ROOT.ML	Fri Sep 24 11:27:15 1993 +0200
     1.2 +++ b/src/ZF/ROOT.ML	Thu Sep 30 10:10:21 1993 +0100
     1.3 @@ -11,20 +11,7 @@
     1.4  val banner = "ZF Set Theory (in FOL)";
     1.5  writeln banner;
     1.6  
     1.7 -(*For Pure/drule??  Multiple resolution infixes*)
     1.8 -infix 0 MRS MRL;
     1.9 -
    1.10 -(*Resolve a list of rules against bottom_rl from right to left*)
    1.11 -fun rls MRS bottom_rl = 
    1.12 -  let fun rs_aux i [] = bottom_rl
    1.13 -	| rs_aux i (rl::rls) = rl RSN (i, rs_aux (i+1) rls)
    1.14 -  in  rs_aux 1 rls  end;
    1.15 -
    1.16 -fun rlss MRL bottom_rls = 
    1.17 -  let fun rs_aux i [] = bottom_rls
    1.18 -	| rs_aux i (rls::rlss) = rls RLN (i, rs_aux (i+1) rlss)
    1.19 -  in  rs_aux 1 rlss  end;
    1.20 -
    1.21 +(*For Pure/tactic??  A crude way of adding structure to rules*)
    1.22  fun CHECK_SOLVED (Tactic tf) = 
    1.23    Tactic (fn state => 
    1.24      case Sequence.pull (tf state) of