--- a/src/ZF/ROOT.ML Thu Jan 07 18:30:55 1999 +0100
+++ b/src/ZF/ROOT.ML Fri Jan 08 13:20:59 1999 +0100
@@ -13,20 +13,6 @@
eta_contract:=false;
-(*For Pure/tactic?? A crude way of adding structure to rules*)
-fun CHECK_SOLVED tac st =
- case Seq.pull (tac st) of
- None => error"DO_GOAL: tactic list failed"
- | Some(x,_) =>
- if has_fewer_prems 1 x then
- Seq.cons(x, Seq.empty)
- else (writeln"DO_GOAL: unsolved goals!!";
- writeln"Final proof state was ...";
- print_goals (!goals_limit) x;
- raise ERROR);
-
-fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs));
-
print_depth 1;
(*Add user sections for inductive/datatype definitions*)