src/Provers/classical.ML
changeset 35625 9c818cab0dd0
parent 35613 9d3ff36ad4e1
child 36546 a9873318fe30
     1.1 --- a/src/Provers/classical.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/Provers/classical.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -153,7 +153,7 @@
     1.4  *)
     1.5  
     1.6  fun classical_rule rule =
     1.7 -  if ObjectLogic.is_elim rule then
     1.8 +  if Object_Logic.is_elim rule then
     1.9      let
    1.10        val rule' = rule RS classical;
    1.11        val concl' = Thm.concl_of rule';
    1.12 @@ -173,7 +173,7 @@
    1.13    else rule;
    1.14  
    1.15  (*flatten nested meta connectives in prems*)
    1.16 -val flat_rule = Conv.fconv_rule (Conv.prems_conv ~1 ObjectLogic.atomize_prems);
    1.17 +val flat_rule = Conv.fconv_rule (Conv.prems_conv ~1 Object_Logic.atomize_prems);
    1.18  
    1.19  
    1.20  (*** Useful tactics for classical reasoning ***)
    1.21 @@ -724,24 +724,24 @@
    1.22  
    1.23  (*Dumb but fast*)
    1.24  fun fast_tac cs =
    1.25 -  ObjectLogic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
    1.26 +  Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
    1.27  
    1.28  (*Slower but smarter than fast_tac*)
    1.29  fun best_tac cs =
    1.30 -  ObjectLogic.atomize_prems_tac THEN'
    1.31 +  Object_Logic.atomize_prems_tac THEN'
    1.32    SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
    1.33  
    1.34  (*even a bit smarter than best_tac*)
    1.35  fun first_best_tac cs =
    1.36 -  ObjectLogic.atomize_prems_tac THEN'
    1.37 +  Object_Logic.atomize_prems_tac THEN'
    1.38    SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs)));
    1.39  
    1.40  fun slow_tac cs =
    1.41 -  ObjectLogic.atomize_prems_tac THEN'
    1.42 +  Object_Logic.atomize_prems_tac THEN'
    1.43    SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
    1.44  
    1.45  fun slow_best_tac cs =
    1.46 -  ObjectLogic.atomize_prems_tac THEN'
    1.47 +  Object_Logic.atomize_prems_tac THEN'
    1.48    SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1));
    1.49  
    1.50  
    1.51 @@ -749,13 +749,13 @@
    1.52  val weight_ASTAR = Unsynchronized.ref 5;
    1.53  
    1.54  fun astar_tac cs =
    1.55 -  ObjectLogic.atomize_prems_tac THEN'
    1.56 +  Object_Logic.atomize_prems_tac THEN'
    1.57    SELECT_GOAL
    1.58      (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
    1.59        (step_tac cs 1));
    1.60  
    1.61  fun slow_astar_tac cs =
    1.62 -  ObjectLogic.atomize_prems_tac THEN'
    1.63 +  Object_Logic.atomize_prems_tac THEN'
    1.64    SELECT_GOAL
    1.65      (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
    1.66        (slow_step_tac cs 1));