--- a/src/ZF/ROOT.ML Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/ROOT.ML Thu Sep 30 10:10:21 1993 +0100
@@ -11,20 +11,7 @@
val banner = "ZF Set Theory (in FOL)";
writeln banner;
-(*For Pure/drule?? Multiple resolution infixes*)
-infix 0 MRS MRL;
-
-(*Resolve a list of rules against bottom_rl from right to left*)
-fun rls MRS bottom_rl =
- let fun rs_aux i [] = bottom_rl
- | rs_aux i (rl::rls) = rl RSN (i, rs_aux (i+1) rls)
- in rs_aux 1 rls end;
-
-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;
-
+(*For Pure/tactic?? A crude way of adding structure to rules*)
fun CHECK_SOLVED (Tactic tf) =
Tactic (fn state =>
case Sequence.pull (tf state) of