equal
deleted
inserted
replaced
21 val ITER_DEEPEN : (thm>bool) > (int>tactic) > tactic 
21 val ITER_DEEPEN : (thm>bool) > (int>tactic) > tactic 
22 val THEN_ITER_DEEPEN : tactic > (thm>bool) > (int>tactic) > tactic 
22 val THEN_ITER_DEEPEN : tactic > (thm>bool) > (int>tactic) > tactic 
23 
23 
24 val has_fewer_prems : int > thm > bool 
24 val has_fewer_prems : int > thm > bool 
25 val IF_UNSOLVED : tactic > tactic 
25 val IF_UNSOLVED : tactic > tactic 

26 val SOLVE : tactic > tactic 
26 val trace_BEST_FIRST : bool ref 
27 val trace_BEST_FIRST : bool ref 
27 val BEST_FIRST : (thm > bool) * (thm > int) > tactic > tactic 
28 val BEST_FIRST : (thm > bool) * (thm > int) > tactic > tactic 
28 val THEN_BEST_FIRST : tactic > (thm>bool) * (thm>int) > tactic 
29 val THEN_BEST_FIRST : tactic > (thm>bool) * (thm>int) > tactic 
29 > tactic 
30 > tactic 
30 val trace_ASTAR : bool ref 
31 val trace_ASTAR : bool ref 
62 (*Predicate: Does the rule have fewer than n premises?*) 
63 (*Predicate: Does the rule have fewer than n premises?*) 
63 fun has_fewer_prems n rule = (nprems_of rule < n); 
64 fun has_fewer_prems n rule = (nprems_of rule < n); 
64 
65 
65 (*Apply a tactic if subgoals remain, else do nothing.*) 
66 (*Apply a tactic if subgoals remain, else do nothing.*) 
66 val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac; 
67 val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac; 

68 

69 (*Force a tactic to solve its goal completely, otherwise fail *) 

70 fun SOLVE tac = tac THEN COND (has_fewer_prems 1) all_tac no_tac; 
67 
71 
68 (*Execute tac1, but only execute tac2 if there are at least as many subgoals 
72 (*Execute tac1, but only execute tac2 if there are at least as many subgoals 
69 as before. This ensures that tac2 is only applied to an outcome of tac1.*) 
73 as before. This ensures that tac2 is only applied to an outcome of tac1.*) 
70 fun (tac1 THEN_MAYBE tac2) st = 
74 fun (tac1 THEN_MAYBE tac2) st = 
71 (tac1 THEN COND (has_fewer_prems (nprems_of st)) all_tac tac2) st; 
75 (tac1 THEN COND (has_fewer_prems (nprems_of st)) all_tac tac2) st; 