src/ZF/ROOT.ML
changeset 6071 1b2392ac5752
parent 6070 032babd0120b
child 6112 5e4871c5136b
     1.1 --- a/src/ZF/ROOT.ML	Thu Jan 07 18:30:55 1999 +0100
     1.2 +++ b/src/ZF/ROOT.ML	Fri Jan 08 13:20:59 1999 +0100
     1.3 @@ -13,20 +13,6 @@
     1.4  
     1.5  eta_contract:=false;
     1.6  
     1.7 -(*For Pure/tactic??  A crude way of adding structure to rules*)
     1.8 -fun CHECK_SOLVED tac st =
     1.9 -    case Seq.pull (tac st) of
    1.10 -        None => error"DO_GOAL: tactic list failed"
    1.11 -      | Some(x,_) => 
    1.12 -                if has_fewer_prems 1 x then
    1.13 -                    Seq.cons(x, Seq.empty)
    1.14 -                else (writeln"DO_GOAL: unsolved goals!!";
    1.15 -                      writeln"Final proof state was ...";
    1.16 -                      print_goals (!goals_limit) x;
    1.17 -                      raise ERROR);
    1.18 -
    1.19 -fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs));
    1.20 -
    1.21  print_depth 1;
    1.22  
    1.23  (*Add user sections for inductive/datatype definitions*)