replace sstac
authornipkow
Fri, 09 Feb 1996 13:43:07 +0100
changeset 1487 afc1c1f2523e
parent 1486 7b95d7b49f7a
child 1488 b25a747876a4
replace sstac
src/HOL/ex/set.ML
--- a/src/HOL/ex/set.ML	Fri Feb 09 13:41:59 1996 +0100
+++ b/src/HOL/ex/set.ML	Fri Feb 09 13:43:07 1996 +0100
@@ -89,7 +89,8 @@
 
 val [compl] = goal Lfp.thy
     "Compl(f``X) = g``Compl(X) ==> surj(%z. if z:X then f(z) else g(z))";
-by (sstac [surj_iff_full_range, range_if_then_else, compl RS sym] 1);
+by (EVERY1[stac surj_iff_full_range, stac range_if_then_else,
+           stac (compl RS sym)]);
 by (rtac (X_Un_Compl RS allI) 1);
 qed "surj_if_then_else";