src/HOL/Datatype.thy
changeset 39198 f967a16dfcdd
parent 36176 3fe7e97ccca8
child 39302 d7728f65b353
     1.1 --- a/src/HOL/Datatype.thy	Mon Sep 06 22:58:06 2010 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Tue Sep 07 10:05:19 2010 +0200
     1.3 @@ -109,12 +109,12 @@
     1.4  (** Push -- an injection, analogous to Cons on lists **)
     1.5  
     1.6  lemma Push_inject1: "Push i f = Push j g  ==> i=j"
     1.7 -apply (simp add: Push_def expand_fun_eq) 
     1.8 +apply (simp add: Push_def ext_iff) 
     1.9  apply (drule_tac x=0 in spec, simp) 
    1.10  done
    1.11  
    1.12  lemma Push_inject2: "Push i f = Push j g  ==> f=g"
    1.13 -apply (auto simp add: Push_def expand_fun_eq) 
    1.14 +apply (auto simp add: Push_def ext_iff) 
    1.15  apply (drule_tac x="Suc x" in spec, simp) 
    1.16  done
    1.17  
    1.18 @@ -123,7 +123,7 @@
    1.19  by (blast dest: Push_inject1 Push_inject2) 
    1.20  
    1.21  lemma Push_neq_K0: "Push (Inr (Suc k)) f = (%z. Inr 0) ==> P"
    1.22 -by (auto simp add: Push_def expand_fun_eq split: nat.split_asm)
    1.23 +by (auto simp add: Push_def ext_iff split: nat.split_asm)
    1.24  
    1.25  lemmas Abs_Node_inj = Abs_Node_inject [THEN [2] rev_iffD1, standard]
    1.26  
    1.27 @@ -399,7 +399,7 @@
    1.28  lemma ntrunc_o_equality: 
    1.29      "[| !!k. (ntrunc(k) o h1) = (ntrunc(k) o h2) |] ==> h1=h2"
    1.30  apply (rule ntrunc_equality [THEN ext])
    1.31 -apply (simp add: expand_fun_eq) 
    1.32 +apply (simp add: ext_iff) 
    1.33  done
    1.34  
    1.35