src/HOL/WF.ML
changeset 1552 6f71b5d46700
parent 1485 240cc98b94a7
child 1618 372880456b5b
     1.1 --- a/src/HOL/WF.ML	Wed Mar 06 12:19:16 1996 +0100
     1.2 +++ b/src/HOL/WF.ML	Wed Mar 06 12:52:11 1996 +0100
     1.3 @@ -69,12 +69,12 @@
     1.4    H_cong to expose the equality*)
     1.5  goalw WF.thy [cut_def]
     1.6      "(cut f r x = cut g r x) = (!y. (y,x):r --> f(y)=g(y))";
     1.7 -by(simp_tac (HOL_ss addsimps [expand_fun_eq]
     1.8 +by (simp_tac (HOL_ss addsimps [expand_fun_eq]
     1.9                      setloop (split_tac [expand_if])) 1);
    1.10  qed "cuts_eq";
    1.11  
    1.12  goalw WF.thy [cut_def] "!!x. (x,a):r ==> (cut f r a)(x) = f(x)";
    1.13 -by(asm_simp_tac HOL_ss 1);
    1.14 +by (asm_simp_tac HOL_ss 1);
    1.15  qed "cut_apply";
    1.16  
    1.17  (*** is_recfun ***)
    1.18 @@ -82,7 +82,7 @@
    1.19  goalw WF.thy [is_recfun_def,cut_def]
    1.20      "!!f. [| is_recfun r H a f;  ~(b,a):r |] ==> f(b) = (@z.True)";
    1.21  by (etac ssubst 1);
    1.22 -by(asm_simp_tac HOL_ss 1);
    1.23 +by (asm_simp_tac HOL_ss 1);
    1.24  qed "is_recfun_undef";
    1.25  
    1.26  (*** NOTE! some simplifications need a different finish_tac!! ***)
    1.27 @@ -129,7 +129,7 @@
    1.28    by (wf_ind_tac "a" prems 1);
    1.29    by (res_inst_tac [("f","cut (%y. H (the_recfun r H y) y) r a1")]
    1.30                     is_the_recfun 1);
    1.31 -  by (rewrite_goals_tac [is_recfun_def]);
    1.32 +  by (rewtac is_recfun_def);
    1.33    by (rtac (cuts_eq RS ssubst) 1);
    1.34    by (rtac allI 1);
    1.35    by (rtac impI 1);