src/Provers/classical.ML
changeset 11754 3928d990c22f
parent 11723 2b4a0d630071
child 11783 aee100a086b1
     1.1 --- a/src/Provers/classical.ML	Sun Oct 14 20:02:59 2001 +0200
     1.2 +++ b/src/Provers/classical.ML	Sun Oct 14 20:04:05 2001 +0200
     1.3 @@ -33,7 +33,6 @@
     1.4    val classical : thm           (* (~P ==> P) ==> P *)
     1.5    val sizef     : thm -> int    (* size function for BEST_FIRST *)
     1.6    val hyp_subst_tacs: (int -> tactic) list
     1.7 -  val atomize: thm list
     1.8  end;
     1.9  
    1.10  signature BASIC_CLASSICAL =
    1.11 @@ -182,8 +181,6 @@
    1.12  
    1.13  (*** Useful tactics for classical reasoning ***)
    1.14  
    1.15 -val atomize_tac = Method.atomize_tac atomize;
    1.16 -
    1.17  val imp_elim = (*cannot use bind_thm within a structure!*)
    1.18    store_thm ("imp_elim", Data.make_elim mp);
    1.19  
    1.20 @@ -837,24 +834,24 @@
    1.21  
    1.22  (*Dumb but fast*)
    1.23  fun fast_tac cs =
    1.24 -  atomize_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
    1.25 +  ObjectLogic.atomize_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
    1.26  
    1.27  (*Slower but smarter than fast_tac*)
    1.28  fun best_tac cs =
    1.29 -  atomize_tac THEN'
    1.30 +  ObjectLogic.atomize_tac THEN'
    1.31    SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
    1.32  
    1.33  (*even a bit smarter than best_tac*)
    1.34  fun first_best_tac cs =
    1.35 -  atomize_tac THEN'
    1.36 +  ObjectLogic.atomize_tac THEN'
    1.37    SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs)));
    1.38  
    1.39  fun slow_tac cs =
    1.40 -  atomize_tac THEN'
    1.41 +  ObjectLogic.atomize_tac THEN'
    1.42    SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
    1.43  
    1.44  fun slow_best_tac cs =
    1.45 -  atomize_tac THEN'
    1.46 +  ObjectLogic.atomize_tac THEN'
    1.47    SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1));
    1.48  
    1.49  
    1.50 @@ -862,13 +859,13 @@
    1.51  val weight_ASTAR = ref 5;
    1.52  
    1.53  fun astar_tac cs =
    1.54 -  atomize_tac THEN'
    1.55 +  ObjectLogic.atomize_tac THEN'
    1.56    SELECT_GOAL
    1.57      (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
    1.58        (step_tac cs 1));
    1.59  
    1.60  fun slow_astar_tac cs =
    1.61 -  atomize_tac THEN'
    1.62 +  ObjectLogic.atomize_tac THEN'
    1.63    SELECT_GOAL
    1.64      (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
    1.65        (slow_step_tac cs 1));