# HG changeset patch
# User paulson
# Date 860145631 -7200
# Node ID 67fb21ddfe15ecd2345531b10fae06f93a1a8ff3
# Parent  d8f254ad1ab9a9af0311a5a3b6b69689a7573413
Calls Blast_tac.  Tidied some proofs

diff -r d8f254ad1ab9 -r 67fb21ddfe15 src/HOL/Sexp.ML
--- a/src/HOL/Sexp.ML	Fri Apr 04 11:18:52 1997 +0200
+++ b/src/HOL/Sexp.ML	Fri Apr 04 11:20:31 1997 +0200
@@ -12,17 +12,17 @@
 
 goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
 by (rtac select_equality 1);
-by (ALLGOALS (Fast_tac));
+by (ALLGOALS Blast_tac);
 qed "sexp_case_Leaf";
 
 goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Numb k) = d(k)";
 by (rtac select_equality 1);
-by (ALLGOALS (Fast_tac));
+by (ALLGOALS Blast_tac);
 qed "sexp_case_Numb";
 
 goalw Sexp.thy [sexp_case_def] "sexp_case c d e (M$N) = e M N";
 by (rtac select_equality 1);
-by (ALLGOALS (Fast_tac));
+by (ALLGOALS Blast_tac);
 qed "sexp_case_Scons";
 
 
@@ -41,19 +41,19 @@
 AddIs (sexp.intrs@[SigmaI, uprodI]);
 
 goal Sexp.thy "range(Leaf) <= sexp";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "range_Leaf_subset_sexp";
 
 val [major] = goal Sexp.thy "M$N : sexp ==> M: sexp & N: sexp";
 by (rtac (major RS setup_induction) 1);
 by (etac sexp.induct 1);
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Blast_tac);
 qed "Scons_D";
 
 (** Introduction rules for 'pred_sexp' **)
 
 goalw Sexp.thy [pred_sexp_def] "pred_sexp <= sexp Times sexp";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "pred_sexp_subset_Sigma";
 
 (* (a,b) : pred_sexp^+ ==> a : sexp *)
@@ -62,14 +62,14 @@
 and trancl_pred_sexpD2 = 
     pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2;
 
-val prems = goalw Sexp.thy [pred_sexp_def]
-    "[| M: sexp;  N: sexp |] ==> (M, M$N) : pred_sexp";
-by (fast_tac (!claset addIs prems) 1);
+goalw Sexp.thy [pred_sexp_def]
+    "!!M. [| M: sexp;  N: sexp |] ==> (M, M$N) : pred_sexp";
+by (Blast_tac 1);
 qed "pred_sexpI1";
 
-val prems = goalw Sexp.thy [pred_sexp_def]
-    "[| M: sexp;  N: sexp |] ==> (N, M$N) : pred_sexp";
-by (fast_tac (!claset addIs prems) 1);
+goalw Sexp.thy [pred_sexp_def]
+    "!!M. [| M: sexp;  N: sexp |] ==> (N, M$N) : pred_sexp";
+by (Blast_tac 1);
 qed "pred_sexpI2";
 
 (*Combinations involving transitivity and the rules above*)