src/Provers/classical.ML
changeset 2173 08c68550460b
parent 2066 b9063086ef56
child 2630 7a962f6829ca
equal deleted inserted replaced
2172:61b806c6dabd 2173:08c68550460b
   566 fun DEEPEN tacf m i = STATE(fn state => 
   566 fun DEEPEN tacf m i = STATE(fn state => 
   567    if has_fewer_prems i state then no_tac
   567    if has_fewer_prems i state then no_tac
   568    else (writeln ("Depth = " ^ string_of_int m);
   568    else (writeln ("Depth = " ^ string_of_int m);
   569 	 tacf m i  ORELSE  DEEPEN tacf (m+2) i));
   569 	 tacf m i  ORELSE  DEEPEN tacf (m+2) i));
   570 
   570 
       
   571 (*Search, with depth bound m.  
       
   572   This is the "entry point", which does safe inferences first.*)
   571 fun safe_depth_tac cs m = 
   573 fun safe_depth_tac cs m = 
   572   SUBGOAL 
   574   SUBGOAL 
   573     (fn (prem,i) =>
   575     (fn (prem,i) =>
   574       let val deti =
   576       let val deti =
   575 	  (*No Vars in the goal?  No need to backtrack between goals.*)
   577 	  (*No Vars in the goal?  No need to backtrack between goals.*)