src/ZF/Constructible/Wellorderings.thy
changeset 13352 3cd767f8d78b
parent 13339 0f89104dd377
child 13428 99e52e78eb65
     1.1 --- a/src/ZF/Constructible/Wellorderings.thy	Thu Jul 11 17:56:28 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Fri Jul 12 11:24:40 2002 +0200
     1.3 @@ -161,9 +161,7 @@
     1.4  lemma (in M_axioms) order_isomorphism_abs [simp]: 
     1.5       "[| M(A); M(B); M(f) |] 
     1.6        ==> order_isomorphism(M,A,r,B,s,f) <-> f \<in> ord_iso(A,r,B,s)"
     1.7 -by (simp add: typed_apply_abs [OF bij_is_fun] apply_closed 
     1.8 -              order_isomorphism_def ord_iso_def)
     1.9 -
    1.10 +by (simp add: apply_closed order_isomorphism_def ord_iso_def)
    1.11  
    1.12  lemma (in M_axioms) pred_set_abs [simp]: 
    1.13       "[| M(r); M(B) |] ==> pred_set(M,A,x,r,B) <-> B = Order.pred(A,x,r)"
    1.14 @@ -236,7 +234,7 @@
    1.15  apply (elim conjE CollectE) 
    1.16  apply (erule wellfounded_on_induct, assumption+)
    1.17   apply (insert well_ord_iso_separation [of A f r])
    1.18 - apply (simp add: typed_apply_abs [OF bij_is_fun] apply_closed, clarify) 
    1.19 + apply (simp, clarify) 
    1.20  apply (drule_tac a = x in bij_is_fun [THEN apply_type], assumption, blast)
    1.21  done
    1.22