src/HOL/Univ.ML
changeset 4153 e534c4c32d54
parent 4089 96fba19bcbe2
child 4356 0dfd34f0d33d
     1.1 --- a/src/HOL/Univ.ML	Wed Nov 05 13:14:15 1997 +0100
     1.2 +++ b/src/HOL/Univ.ML	Wed Nov 05 13:23:46 1997 +0100
     1.3 @@ -226,7 +226,7 @@
     1.4      "ndepth (Push_Node i n) = Suc(ndepth(n))";
     1.5  by (stac (Rep_Node RS Node_Push_I RS Abs_Node_inverse) 1);
     1.6  by (cut_facts_tac [rewrite_rule [Node_def] Rep_Node] 1);
     1.7 -by (safe_tac (claset()));
     1.8 +by Safe_tac;
     1.9  by (etac ssubst 1);  (*instantiates type variables!*)
    1.10  by (Simp_tac 1);
    1.11  by (rtac Least_equality 1);
    1.12 @@ -546,7 +546,7 @@
    1.13  (*Dependent version*)
    1.14  goal Univ.thy
    1.15      "(Sigma A B <**> Sigma C D) <= Sigma (A<*>C) (Split(%x y. B(x)<*>D(y)))";
    1.16 -by (safe_tac (claset()));
    1.17 +by Safe_tac;
    1.18  by (stac Split 1);
    1.19  by (Blast_tac 1);
    1.20  qed "dprod_subset_Sigma2";