# HG changeset patch
# User wenzelm
# Date 973283396 -3600
# Node ID 1fb807260ff1bf142a0b1c3f9e4a9aedfa99002e
# Parent  4dfbcad19bfb6d656bcde592a031a0398a4e4109
atomize: all automated tactics that "solve" goals;

diff -r 4dfbcad19bfb -r 1fb807260ff1 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Fri Nov 03 21:28:15 2000 +0100
+++ b/src/Provers/classical.ML	Fri Nov 03 21:29:56 2000 +0100
@@ -33,6 +33,7 @@
   val classical : thm           (* (~P ==> P) ==> P *)
   val sizef     : thm -> int    (* size function for BEST_FIRST *)
   val hyp_subst_tacs: (int -> tactic) list
+  val atomize: thm list
 end;
 
 signature BASIC_CLASSICAL =
@@ -182,6 +183,8 @@
 
 (*** Useful tactics for classical reasoning ***)
 
+val atomize_tac = Method.atomize_tac atomize;
+
 val imp_elim = (*cannot use bind_thm within a structure!*)
   store_thm ("imp_elim", Data.make_elim mp);
 
@@ -832,34 +835,42 @@
 (**** The following tactics all fail unless they solve one goal ****)
 
 (*Dumb but fast*)
-fun fast_tac cs = SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
+fun fast_tac cs =
+  atomize_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
 
 (*Slower but smarter than fast_tac*)
-fun best_tac cs = 
+fun best_tac cs =
+  atomize_tac THEN'
   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
 
 (*even a bit smarter than best_tac*)
-fun first_best_tac cs = 
+fun first_best_tac cs =
+  atomize_tac THEN'
   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs)));
 
-fun slow_tac cs = SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
+fun slow_tac cs =
+  atomize_tac THEN'
+  SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
 
-fun slow_best_tac cs = 
+fun slow_best_tac cs =
+  atomize_tac THEN'
   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1));
 
 
 (***ASTAR with weight weight_ASTAR, by Norbert Voelker*) 
 val weight_ASTAR = ref 5; 
 
-fun astar_tac cs = 
-  SELECT_GOAL ( ASTAR (has_fewer_prems 1
-              , fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) 
-              (step_tac cs 1));
+fun astar_tac cs =
+  atomize_tac THEN' 
+  SELECT_GOAL
+    (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
+      (step_tac cs 1));
 
 fun slow_astar_tac cs = 
-  SELECT_GOAL ( ASTAR (has_fewer_prems 1
-              , fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) 
-              (slow_step_tac cs 1));
+  atomize_tac THEN' 
+  SELECT_GOAL
+    (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
+      (slow_step_tac cs 1));
 
 (**** Complete tactic, loosely based upon LeanTaP.  This tactic is the outcome
   of much experimentation!  Changing APPEND to ORELSE below would prove
@@ -1111,12 +1122,14 @@
 fun rule_tac [] cs facts = some_rule_tac cs facts
   | rule_tac rules _ facts = Method.rule_tac rules facts;
 
-fun default_tac rules cs facts =
-  rule_tac rules cs facts ORELSE' AxClass.default_intro_classes_tac facts;
+fun default_tac rules ctxt cs facts =
+  rule_tac rules cs facts ORELSE'
+  Method.some_rule_tac rules ctxt facts ORELSE'
+  AxClass.default_intro_classes_tac facts;
 
 in
   val rule = METHOD_CLASET' o rule_tac;
-  val default = METHOD_CLASET' o default_tac;
+  fun default rules ctxt = METHOD_CLASET' (default_tac rules ctxt) ctxt;
 end;