author | nipkow |
Fri, 09 Feb 1996 13:43:07 +0100 | |
changeset 1487 | afc1c1f2523e |
parent 1486 | 7b95d7b49f7a |
child 1488 | b25a747876a4 |
src/HOL/ex/set.ML | file | annotate | diff | comparison | revisions |
--- 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";