--- 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) =