src/HOL/Sexp.ML
changeset 2892 67fb21ddfe15
parent 2089 e2ec077ac90d
child 3029 db0e9b30dc92
     1.1 --- a/src/HOL/Sexp.ML	Fri Apr 04 11:18:52 1997 +0200
     1.2 +++ b/src/HOL/Sexp.ML	Fri Apr 04 11:20:31 1997 +0200
     1.3 @@ -12,17 +12,17 @@
     1.4  
     1.5  goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
     1.6  by (rtac select_equality 1);
     1.7 -by (ALLGOALS (Fast_tac));
     1.8 +by (ALLGOALS Blast_tac);
     1.9  qed "sexp_case_Leaf";
    1.10  
    1.11  goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Numb k) = d(k)";
    1.12  by (rtac select_equality 1);
    1.13 -by (ALLGOALS (Fast_tac));
    1.14 +by (ALLGOALS Blast_tac);
    1.15  qed "sexp_case_Numb";
    1.16  
    1.17  goalw Sexp.thy [sexp_case_def] "sexp_case c d e (M$N) = e M N";
    1.18  by (rtac select_equality 1);
    1.19 -by (ALLGOALS (Fast_tac));
    1.20 +by (ALLGOALS Blast_tac);
    1.21  qed "sexp_case_Scons";
    1.22  
    1.23  
    1.24 @@ -41,19 +41,19 @@
    1.25  AddIs (sexp.intrs@[SigmaI, uprodI]);
    1.26  
    1.27  goal Sexp.thy "range(Leaf) <= sexp";
    1.28 -by (Fast_tac 1);
    1.29 +by (Blast_tac 1);
    1.30  qed "range_Leaf_subset_sexp";
    1.31  
    1.32  val [major] = goal Sexp.thy "M$N : sexp ==> M: sexp & N: sexp";
    1.33  by (rtac (major RS setup_induction) 1);
    1.34  by (etac sexp.induct 1);
    1.35 -by (ALLGOALS Fast_tac);
    1.36 +by (ALLGOALS Blast_tac);
    1.37  qed "Scons_D";
    1.38  
    1.39  (** Introduction rules for 'pred_sexp' **)
    1.40  
    1.41  goalw Sexp.thy [pred_sexp_def] "pred_sexp <= sexp Times sexp";
    1.42 -by (Fast_tac 1);
    1.43 +by (Blast_tac 1);
    1.44  qed "pred_sexp_subset_Sigma";
    1.45  
    1.46  (* (a,b) : pred_sexp^+ ==> a : sexp *)
    1.47 @@ -62,14 +62,14 @@
    1.48  and trancl_pred_sexpD2 = 
    1.49      pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2;
    1.50  
    1.51 -val prems = goalw Sexp.thy [pred_sexp_def]
    1.52 -    "[| M: sexp;  N: sexp |] ==> (M, M$N) : pred_sexp";
    1.53 -by (fast_tac (!claset addIs prems) 1);
    1.54 +goalw Sexp.thy [pred_sexp_def]
    1.55 +    "!!M. [| M: sexp;  N: sexp |] ==> (M, M$N) : pred_sexp";
    1.56 +by (Blast_tac 1);
    1.57  qed "pred_sexpI1";
    1.58  
    1.59 -val prems = goalw Sexp.thy [pred_sexp_def]
    1.60 -    "[| M: sexp;  N: sexp |] ==> (N, M$N) : pred_sexp";
    1.61 -by (fast_tac (!claset addIs prems) 1);
    1.62 +goalw Sexp.thy [pred_sexp_def]
    1.63 +    "!!M. [| M: sexp;  N: sexp |] ==> (N, M$N) : pred_sexp";
    1.64 +by (Blast_tac 1);
    1.65  qed "pred_sexpI2";
    1.66  
    1.67  (*Combinations involving transitivity and the rules above*)