src/ZF/OrderArith.thy
changeset 13784 b9f6154427a4
parent 13634 99a593b49b04
child 13823 d49ffd9f9662
     1.1 --- a/src/ZF/OrderArith.thy	Thu Jan 23 09:16:53 2003 +0100
     1.2 +++ b/src/ZF/OrderArith.thy	Thu Jan 23 10:30:14 2003 +0100
     1.3 @@ -88,12 +88,12 @@
     1.4   prefer 2
     1.5   apply (erule_tac V = "y : A + B" in thin_rl)
     1.6   apply (rule_tac ballI)
     1.7 - apply (erule_tac r = "r" and a = "x" in wf_on_induct, assumption)
     1.8 + apply (erule_tac r = r and a = x in wf_on_induct, assumption)
     1.9   apply blast 
    1.10  txt{*Returning to main part of proof*}
    1.11  apply safe
    1.12  apply blast
    1.13 -apply (erule_tac r = "s" and a = "ya" in wf_on_induct, assumption, blast) 
    1.14 +apply (erule_tac r = s and a = ya in wf_on_induct, assumption, blast) 
    1.15  done
    1.16  
    1.17  lemma wf_radd: "[| wf(r);  wf(s) |] ==> wf(radd(field(r),r,field(s),s))"
    1.18 @@ -193,9 +193,9 @@
    1.19  apply (erule SigmaE)
    1.20  apply (erule ssubst)
    1.21  apply (subgoal_tac "ALL b:B. <x,b>: Ba", blast)
    1.22 -apply (erule_tac a = "x" in wf_on_induct, assumption)
    1.23 +apply (erule_tac a = x in wf_on_induct, assumption)
    1.24  apply (rule ballI)
    1.25 -apply (erule_tac a = "b" in wf_on_induct, assumption)
    1.26 +apply (erule_tac a = b in wf_on_induct, assumption)
    1.27  apply (best elim!: rmultE bspec [THEN mp])
    1.28  done
    1.29  
    1.30 @@ -236,7 +236,7 @@
    1.31  done
    1.32  
    1.33  lemma singleton_prod_bij: "(lam z:A. <x,z>) : bij(A, {x}*A)"
    1.34 -by (rule_tac d = "snd" in lam_bijective, auto)
    1.35 +by (rule_tac d = snd in lam_bijective, auto)
    1.36  
    1.37  (*Used??*)
    1.38  lemma singleton_prod_ord_iso:
    1.39 @@ -310,8 +310,7 @@
    1.40  subsubsection{*Type checking*}
    1.41  
    1.42  lemma rvimage_type: "rvimage(A,f,r) <= A*A"
    1.43 -apply (unfold rvimage_def, rule Collect_subset)
    1.44 -done
    1.45 +by (unfold rvimage_def, rule Collect_subset)
    1.46  
    1.47  lemmas field_rvimage = rvimage_type [THEN field_rel_subset]
    1.48  
    1.49 @@ -539,8 +538,7 @@
    1.50  apply (rename_tac u) 
    1.51  apply (drule_tac x=u in bspec, blast) 
    1.52  apply (erule mp, clarify)
    1.53 -apply (frule ok, assumption+); 
    1.54 -apply blast 
    1.55 +apply (frule ok, assumption+, blast) 
    1.56  done
    1.57  
    1.58