1.1 --- a/src/Provers/classical.ML	Tue Feb 20 18:47:30 2001 +0100
     1.2 +++ b/src/Provers/classical.ML	Tue Feb 20 18:47:32 2001 +0100
     1.3 @@ -712,13 +712,13 @@
     1.4      in if null del then (warning ("No such unsafe wrapper in claset: " ^ name);
     1.5                           uwrappers) else rest end);
     1.6  
     1.7 -(*compose a safe tactic sequentially before/alternatively after safe_step_tac*)
     1.8 +(* compose a safe tactic alternatively before/after safe_step_tac *)
     1.9  fun cs addSbefore  (name,    tac1) =
    1.10      cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2);
    1.11  fun cs addSaltern  (name,    tac2) =
    1.12      cs addSWrapper (name, fn tac1 => tac1 ORELSE' tac2);
    1.13  
    1.14 -(*compose a tactic sequentially before/alternatively after the step tactic*)
    1.15 +(*compose a tactic alternatively before/after the step tactic *)
    1.16  fun cs addbefore   (name,    tac1) =
    1.17      cs addWrapper  (name, fn tac2 => tac1 APPEND' tac2);
    1.18  fun cs addaltern   (name,    tac2) =