src/HOL/Sexp.ML
changeset 2031 03a843f0f447
parent 1985 84cf16192e03
child 2089 e2ec077ac90d
     1.1 --- a/src/HOL/Sexp.ML	Thu Sep 26 11:11:22 1996 +0200
     1.2 +++ b/src/HOL/Sexp.ML	Thu Sep 26 12:47:47 1996 +0200
     1.3 @@ -11,17 +11,17 @@
     1.4  (** sexp_case **)
     1.5  
     1.6  goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
     1.7 -by (resolve_tac [select_equality] 1);
     1.8 +by (rtac select_equality 1);
     1.9  by (ALLGOALS (Fast_tac));
    1.10  qed "sexp_case_Leaf";
    1.11  
    1.12  goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Numb k) = d(k)";
    1.13 -by (resolve_tac [select_equality] 1);
    1.14 +by (rtac select_equality 1);
    1.15  by (ALLGOALS (Fast_tac));
    1.16  qed "sexp_case_Numb";
    1.17  
    1.18  goalw Sexp.thy [sexp_case_def] "sexp_case c d e (M$N) = e M N";
    1.19 -by (resolve_tac [select_equality] 1);
    1.20 +by (rtac select_equality 1);
    1.21  by (ALLGOALS (Fast_tac));
    1.22  qed "sexp_case_Scons";
    1.23