--- a/src/ZF/AC/AC_Equiv.ML Fri Sep 18 15:09:26 1998 +0200
+++ b/src/ZF/AC/AC_Equiv.ML Fri Sep 18 15:09:46 1998 +0200
@@ -95,8 +95,7 @@
qed "Inf_Card_is_InfCard";
Goal "(THE z. {x}={z}) = x";
-by (fast_tac (claset() addSIs [the_equality]
- addSEs [singleton_eq_iff RS iffD1 RS sym]) 1);
+by (fast_tac (claset() addSEs [singleton_eq_iff RS iffD1 RS sym]) 1);
qed "the_element";
Goal "(lam x:A. {x}) : bij(A, {{x}. x:A})";
--- a/src/ZF/AC/WO6_WO1.ML Fri Sep 18 15:09:26 1998 +0200
+++ b/src/ZF/AC/WO6_WO1.ML Fri Sep 18 15:09:46 1998 +0200
@@ -396,7 +396,7 @@
by (dtac lemma1 1 THEN REPEAT (assume_tac 1));
by (fast_tac (claset() addSEs [Least_le RS lt_trans1 RS ltD, lt_Ord]) 1);
by (resolve_tac [lemma2 RS ssubst] 1 THEN REPEAT (assume_tac 1));
-by (fast_tac (claset() addSIs [the_equality]) 1);
+by (Blast_tac 1);
qed "NN_imp_ex_inj";
Goal "[| y*y <= y; 1 : NN(y) |] ==> EX r. well_ord(y, r)";
--- a/src/ZF/Epsilon.ML Fri Sep 18 15:09:26 1998 +0200
+++ b/src/ZF/Epsilon.ML Fri Sep 18 15:09:46 1998 +0200
@@ -289,8 +289,7 @@
by (rtac arg_subset_eclose 1);
qed "eclose_idem";
-(*Transfinite recursion for definitions based on the three cases of ordinals.
-*)
+(*Transfinite recursion for definitions based on the three cases of ordinals*)
Goal "transrec2(0,a,b) = a";
by (rtac (transrec2_def RS def_transrec RS trans) 1);
@@ -298,7 +297,7 @@
qed "transrec2_0";
Goal "(THE j. i=j) = i";
-by (blast_tac (claset() addSIs [the_equality]) 1);
+by (Blast_tac 1);
qed "THE_eq";
Goal "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))";
--- a/src/ZF/Nat.ML Fri Sep 18 15:09:26 1998 +0200
+++ b/src/ZF/Nat.ML Fri Sep 18 15:09:46 1998 +0200
@@ -3,7 +3,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-For nat.thy. Natural numbers in Zermelo-Fraenkel Set Theory
+Natural numbers in Zermelo-Fraenkel Set Theory
*)
open Nat;
@@ -193,11 +193,11 @@
(** nat_case **)
Goalw [nat_case_def] "nat_case(a,b,0) = a";
-by (blast_tac (claset() addIs [the_equality]) 1);
+by (Blast_tac 1);
qed "nat_case_0";
Goalw [nat_case_def] "nat_case(a,b,succ(m)) = b(m)";
-by (blast_tac (claset() addIs [the_equality]) 1);
+by (Blast_tac 1);
qed "nat_case_succ";
Addsimps [nat_case_0, nat_case_succ];
--- a/src/ZF/QPair.ML Fri Sep 18 15:09:26 1998 +0200
+++ b/src/ZF/QPair.ML Fri Sep 18 15:09:46 1998 +0200
@@ -98,11 +98,11 @@
qed_goalw "qfst_conv" thy [qfst_def] "qfst(<a;b>) = a"
(fn _=>
- [ (blast_tac (claset() addIs [the_equality]) 1) ]);
+ [ (Blast_tac 1) ]);
qed_goalw "qsnd_conv" thy [qsnd_def] "qsnd(<a;b>) = b"
(fn _=>
- [ (blast_tac (claset() addIs [the_equality]) 1) ]);
+ [ (Blast_tac 1) ]);
Addsimps [qfst_conv, qsnd_conv];
--- a/src/ZF/Resid/Residuals.ML Fri Sep 18 15:09:26 1998 +0200
+++ b/src/ZF/Resid/Residuals.ML Fri Sep 18 15:09:46 1998 +0200
@@ -5,14 +5,12 @@
Logic Image: ZF
*)
-open Residuals;
-
(* ------------------------------------------------------------------------- *)
(* Setting up rule lists *)
(* ------------------------------------------------------------------------- *)
-AddIs (Sres.intrs@redexes.intrs@Sreg.intrs@
- [subst_type]@nat_typechecks);
+AddIs (Sres.intrs @ redexes.intrs @ Sreg.intrs @
+ [subst_type] @ nat_typechecks);
AddSEs (redexes.free_SEs @
(map (Sres.mk_cases redexes.con_defs)
["residuals(Var(n),Var(n),v)",
@@ -53,14 +51,14 @@
by (ALLGOALS Fast_tac);
qed "residuals_intro";
-val prems = goal Residuals.thy
- "[|u~v; residuals(u,v,THE w. residuals(u, v, w))==> R; \
-\ regular(v)|] ==> R";
+val prems =
+Goal "[| u~v; residuals(u,v,THE w. residuals(u, v, w))==> R; \
+\ regular(v) |] ==> R";
by (cut_facts_tac prems 1);
by (resolve_tac prems 1);
by (resolve_tac [residuals_intro RS mp RS exE] 1);
-by (resolve_tac [the_equality RS ssubst] 3);
-by (ALLGOALS (fast_tac (claset() addIs [residuals_function])));
+by (stac the_equality 3);
+by (ALLGOALS (blast_tac (claset() addIs [residuals_function])));
qed "comp_resfuncE";
@@ -68,29 +66,29 @@
(* Residual function *)
(* ------------------------------------------------------------------------- *)
-val resfunc_cs = (claset() addIs [the_equality,residuals_function]
- addSEs [comp_resfuncE]);
-
Goalw [res_func_def]
"n:nat ==> Var(n) |> Var(n) = Var(n)";
-by (fast_tac resfunc_cs 1);
+by (Blast_tac 1);
qed "res_Var";
Goalw [res_func_def]
"[|s~t; regular(t)|]==> Fun(s) |> Fun(t) = Fun(s |> t)";
-by (fast_tac resfunc_cs 1);
+by (blast_tac (claset() addSEs [comp_resfuncE]
+ addIs [residuals_function]) 1);
qed "res_Fun";
Goalw [res_func_def]
"[|s~u; regular(u); t~v; regular(v); b:bool|]==> \
\ App(b,s,t) |> App(0,u,v) = App(b, s |> u, t |> v)";
-by (fast_tac resfunc_cs 1);
+by (blast_tac (claset() addSEs [comp_resfuncE]
+ addIs [residuals_function]) 1);
qed "res_App";
Goalw [res_func_def]
"[|s~u; regular(u); t~v; regular(v); b:bool|]==> \
\ App(b,Fun(s),t) |> App(1,Fun(u),v) = (t |> v)/ (s |> u)";
-by (fast_tac resfunc_cs 1);
+by (blast_tac (claset() addSEs [comp_resfuncE]
+ addIs [residuals_function]) 1);
qed "res_redex";
Goal "[|s~t; regular(t)|]==> regular(t) --> s |> t:redexes";
--- a/src/ZF/ex/Rmap.ML Fri Sep 18 15:09:26 1998 +0200
+++ b/src/ZF/ex/Rmap.ML Fri Sep 18 15:09:46 1998 +0200
@@ -48,7 +48,7 @@
qed "rmap_fun_type";
Goalw [apply_def] "rmap(f)`Nil = Nil";
-by (fast_tac (claset() addIs [the_equality]) 1);
+by (Blast_tac 1);
qed "rmap_Nil";
Goal "[| f: A->B; x: A; xs: list(A) |] ==> \
--- a/src/ZF/func.ML Fri Sep 18 15:09:26 1998 +0200
+++ b/src/ZF/func.ML Fri Sep 18 15:09:46 1998 +0200
@@ -70,14 +70,12 @@
(*** Function Application ***)
-Goalw [Pi_def, function_def]
- "[| <a,b>: f; <a,c>: f; f: Pi(A,B) |] ==> b=c";
+Goalw [Pi_def, function_def] "[| <a,b>: f; <a,c>: f; f: Pi(A,B) |] ==> b=c";
by (Blast_tac 1);
qed "apply_equality2";
-Goalw [apply_def, function_def]
- "[| <a,b>: f; function(f) |] ==> f`a = b";
-by (blast_tac (claset() addIs [the_equality]) 1);
+Goalw [apply_def, function_def] "[| <a,b>: f; function(f) |] ==> f`a = b";
+by (Blast_tac 1);
qed "function_apply_equality";
Goalw [Pi_def] "[| <a,b>: f; f: Pi(A,B) |] ==> f`a = b";
@@ -85,8 +83,7 @@
qed "apply_equality";
(*Applying a function outside its domain yields 0*)
-Goalw [apply_def]
- "a ~: domain(f) ==> f`a = 0";
+Goalw [apply_def] "a ~: domain(f) ==> f`a = 0";
by (rtac the_0 1);
by (Blast_tac 1);
qed "apply_0";
--- a/src/ZF/pair.ML Fri Sep 18 15:09:26 1998 +0200
+++ b/src/ZF/pair.ML Fri Sep 18 15:09:46 1998 +0200
@@ -114,10 +114,10 @@
(*** Projections: fst, snd ***)
qed_goalw "fst_conv" thy [fst_def] "fst(<a,b>) = a"
- (fn _=> [ (blast_tac (claset() addIs [the_equality]) 1) ]);
+ (fn _=> [ (Blast_tac 1) ]);
qed_goalw "snd_conv" thy [snd_def] "snd(<a,b>) = b"
- (fn _=> [ (blast_tac (claset() addIs [the_equality]) 1) ]);
+ (fn _=> [ (Blast_tac 1) ]);
Addsimps [fst_conv,snd_conv];