src/ZF/ROOT.ML
changeset 5 75e163863e16
parent 0 a5a9c433f639
child 6 8ce8c4d13d4d
     1.1 --- a/src/ZF/ROOT.ML	Thu Sep 16 17:41:10 1993 +0200
     1.2 +++ b/src/ZF/ROOT.ML	Fri Sep 17 12:53:53 1993 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title: 	ZF/ROOT
     1.5 -    ID:         $Id$
     1.6      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7      Copyright   1993  University of Cambridge
     1.8  
     1.9 @@ -25,6 +24,20 @@
    1.10  	| rs_aux i (rls::rlss) = rls RLN (i, rs_aux (i+1) rlss)
    1.11    in  rs_aux 1 rlss  end;
    1.12  
    1.13 +fun CHECK_SOLVED (Tactic tf) = 
    1.14 +  Tactic (fn state => 
    1.15 +    case Sequence.pull (tf state) of
    1.16 +	None => error"DO_GOAL: tactic list failed"
    1.17 +      | Some(x,_) => 
    1.18 +		if has_fewer_prems 1 x then
    1.19 +		    Sequence.cons(x, Sequence.null)
    1.20 +		else (writeln"DO_GOAL: unsolved goals!!";
    1.21 +		      writeln"Final proof state was ...";
    1.22 +		      print_goals (!goals_limit) x;
    1.23 +		      raise ERROR));
    1.24 +
    1.25 +fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs));
    1.26 +
    1.27  print_depth 1;
    1.28  use_thy "zf";
    1.29