src/HOL/WF.ML
changeset 4686 74a12e86b20b
parent 4350 1983e4054fd8
child 4746 a5dcd7e4a37d
     1.1 --- a/src/HOL/WF.ML	Fri Mar 06 18:25:28 1998 +0100
     1.2 +++ b/src/HOL/WF.ML	Sat Mar 07 16:29:29 1998 +0100
     1.3 @@ -153,7 +153,7 @@
     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] addsplits [expand_if]) 1);
     1.8 +by (simp_tac (HOL_ss addsimps [expand_fun_eq]) 1);
     1.9  qed "cuts_eq";
    1.10  
    1.11  goalw WF.thy [cut_def] "!!x. (x,a):r ==> (cut f r a)(x) = f(x)";
    1.12 @@ -193,8 +193,7 @@
    1.13  and fisg   = recgb RS (recfa RS (transr RS (wfr RS is_recfun_equal)));
    1.14  by (cut_facts_tac prems 1);
    1.15  by (rtac ext 1);
    1.16 -by (asm_simp_tac (wf_super_ss addsimps [gundef,fisg]
    1.17 -                              addsplits [expand_if]) 1);
    1.18 +by (asm_simp_tac (wf_super_ss addsimps [gundef,fisg]) 1);
    1.19  qed "is_recfun_cut";
    1.20  
    1.21  (*** Main Existence Lemma -- Basic Properties of the_recfun ***)