# HG changeset patch # User paulson # Date 906124186 -7200 # Node ID b0856ff6fc6938a0491435bb992c83f6f295cd41 # Parent 739b777e435511a32c95c7a7d6f1dcbe7b4ee35c tidied diff -r 739b777e4355 -r b0856ff6fc69 src/ZF/AC/AC_Equiv.ML --- 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})"; diff -r 739b777e4355 -r b0856ff6fc69 src/ZF/AC/WO6_WO1.ML --- 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)"; diff -r 739b777e4355 -r b0856ff6fc69 src/ZF/Epsilon.ML --- 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))"; diff -r 739b777e4355 -r b0856ff6fc69 src/ZF/Nat.ML --- 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]; diff -r 739b777e4355 -r b0856ff6fc69 src/ZF/QPair.ML --- 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" (fn _=> - [ (blast_tac (claset() addIs [the_equality]) 1) ]); + [ (Blast_tac 1) ]); qed_goalw "qsnd_conv" thy [qsnd_def] "qsnd() = b" (fn _=> - [ (blast_tac (claset() addIs [the_equality]) 1) ]); + [ (Blast_tac 1) ]); Addsimps [qfst_conv, qsnd_conv]; diff -r 739b777e4355 -r b0856ff6fc69 src/ZF/Resid/Residuals.ML --- 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"; diff -r 739b777e4355 -r b0856ff6fc69 src/ZF/ex/Rmap.ML --- 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) |] ==> \ diff -r 739b777e4355 -r b0856ff6fc69 src/ZF/func.ML --- 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] - "[| : f; : f; f: Pi(A,B) |] ==> b=c"; +Goalw [Pi_def, function_def] "[| : f; : f; f: Pi(A,B) |] ==> b=c"; by (Blast_tac 1); qed "apply_equality2"; -Goalw [apply_def, function_def] - "[| : f; function(f) |] ==> f`a = b"; -by (blast_tac (claset() addIs [the_equality]) 1); +Goalw [apply_def, function_def] "[| : f; function(f) |] ==> f`a = b"; +by (Blast_tac 1); qed "function_apply_equality"; Goalw [Pi_def] "[| : 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"; diff -r 739b777e4355 -r b0856ff6fc69 src/ZF/pair.ML --- 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" - (fn _=> [ (blast_tac (claset() addIs [the_equality]) 1) ]); + (fn _=> [ (Blast_tac 1) ]); qed_goalw "snd_conv" thy [snd_def] "snd() = b" - (fn _=> [ (blast_tac (claset() addIs [the_equality]) 1) ]); + (fn _=> [ (Blast_tac 1) ]); Addsimps [fst_conv,snd_conv];