Univ.ML

 by (etac (singleton_inject RS Abs_Node_inject RS Pair_inject) 1);
 by (REPEAT (ares_tac [Node_K0_I] 1));
 val inj_Atom = result();
 val Atom_inject = inj_Atom RS injD;
 
-goalw Univ.thy [Leaf_def] "inj(Leaf)";
-by (stac o_def 1);
+goalw Univ.thy [Leaf_def,o_def] "inj(Leaf)";
 by (rtac injI 1);
 by (etac (Atom_inject RS Inl_inject) 1);
 val inj_Leaf = result();
 
 val Leaf_inject = inj_Leaf RS injD;
 
-goalw Univ.thy [Numb_def] "inj(Numb)";
-by (stac o_def 1);
+goalw Univ.thy [Numb_def,o_def] "inj(Numb)";
 by (rtac injI 1);
 by (etac (Atom_inject RS Inr_inject) 1);
 val inj_Numb = result();
 
 val Numb_inject = inj_Numb RS injD;

 
 (*** Distinctness involving Leaf and Numb ***)
 
 (** Scons vs Leaf **)
 
-goalw Univ.thy [Leaf_def] "(M$N) ~= Leaf(a)";
-by (stac o_def 1);
+goalw Univ.thy [Leaf_def,o_def] "(M$N) ~= Leaf(a)";
 by (rtac Scons_not_Atom 1);
 val Scons_not_Leaf = result();
 val Leaf_not_Scons = standard (Scons_not_Leaf RS not_sym);
 
 val Scons_neq_Leaf = standard (Scons_not_Leaf RS notE);
 val Leaf_neq_Scons = sym RS Scons_neq_Leaf;
 
 (** Scons vs Numb **)
 
-goalw Univ.thy [Numb_def] "(M$N) ~= Numb(k)";
-by (stac o_def 1);
+goalw Univ.thy [Numb_def,o_def] "(M$N) ~= Numb(k)";
 by (rtac Scons_not_Atom 1);
 val Scons_not_Numb = result();
 val Numb_not_Scons = standard (Scons_not_Numb RS not_sym);
 
 val Scons_neq_Numb = standard (Scons_not_Numb RS notE);

 by (safe_tac (set_cs addSIs [equalityI]));
 by (stac ndepth_K0 1);
 by (rtac zero_less_Suc 1);
 val ntrunc_Atom = result();
 
-goalw Univ.thy [Leaf_def] "ntrunc(Suc(k), Leaf(a)) = Leaf(a)";
-by (stac o_def 1);
+goalw Univ.thy [Leaf_def,o_def] "ntrunc(Suc(k), Leaf(a)) = Leaf(a)";
 by (rtac ntrunc_Atom 1);
 val ntrunc_Leaf = result();
 
-goalw Univ.thy [Numb_def] "ntrunc(Suc(k), Numb(i)) = Numb(i)";
-by (stac o_def 1);
+goalw Univ.thy [Numb_def,o_def] "ntrunc(Suc(k), Numb(i)) = Numb(i)";
 by (rtac ntrunc_Atom 1);
 val ntrunc_Numb = result();
 
 goalw Univ.thy [Scons_def,ntrunc_def]
     "ntrunc(Suc(k), M$N) = ntrunc(k,M) $ ntrunc(k,N)";

 by (ALLGOALS (rtac (ntrunc_subsetI RSN (2, subset_trans))));
 by (rtac (major RS equalityD1) 1);
 by (rtac (major RS equalityD2) 1);
 val ntrunc_equality = result();
 
-val [major] = goal Univ.thy
+val [major] = goalw Univ.thy [o_def]
     "[| !!k. (ntrunc(k) o h1) = (ntrunc(k) o h2) |] ==> h1=h2";
 by (rtac (ntrunc_equality RS ext) 1);
-by (resolve_tac ([major RS fun_cong] RL [o_def RS subst]) 1);
+by (rtac (major RS fun_cong) 1);
 val ntrunc_o_equality = result();
 
 (*** Monotonicity ***)
 
 goalw Univ.thy [uprod_def] "!!A B. [| A<=A';  B<=B' |] ==> A<*>B <= A'<*>B'";