# HG changeset patch
# User oheimb
# Date 982691252 -3600
# Node ID b964accc93074946d26a4478369270e89694be6d
# Parent  2c90a6167b0b1590e6de5691c9dfd26aed49cd02
corrected comments on addbefore and addSbefore

diff -r 2c90a6167b0b -r b964accc9307 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue Feb 20 18:47:30 2001 +0100
+++ b/src/Provers/classical.ML	Tue Feb 20 18:47:32 2001 +0100
@@ -712,13 +712,13 @@
     in if null del then (warning ("No such unsafe wrapper in claset: " ^ name);
                          uwrappers) else rest end);
 
-(*compose a safe tactic sequentially before/alternatively after safe_step_tac*)
+(* compose a safe tactic alternatively before/after safe_step_tac *)
 fun cs addSbefore  (name,    tac1) =
     cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2);
 fun cs addSaltern  (name,    tac2) =
     cs addSWrapper (name, fn tac1 => tac1 ORELSE' tac2);
 
-(*compose a tactic sequentially before/alternatively after the step tactic*)
+(*compose a tactic alternatively before/after the step tactic *)
 fun cs addbefore   (name,    tac1) =
     cs addWrapper  (name, fn tac2 => tac1 APPEND' tac2);
 fun cs addaltern   (name,    tac2) =