src/ZF/OrderArith.thy
changeset 22710 f44439cdce77
parent 16417 9bc16273c2d4
child 24893 b8ef7afe3a6b
     1.1 --- a/src/ZF/OrderArith.thy	Sun Apr 15 23:25:50 2007 +0200
     1.2 +++ b/src/ZF/OrderArith.thy	Sun Apr 15 23:25:52 2007 +0200
     1.3 @@ -369,7 +369,7 @@
     1.4  done
     1.5  
     1.6  text{*But note that the combination of @{text wf_imp_wf_on} and
     1.7 - @{text wf_rvimage} gives @{term "wf(r) ==> wf[C](rvimage(A,f,r))"}*}
     1.8 + @{text wf_rvimage} gives @{prop "wf(r) ==> wf[C](rvimage(A,f,r))"}*}
     1.9  lemma wf_on_rvimage: "[| f: A->B;  wf[B](r) |] ==> wf[A](rvimage(A,f,r))"
    1.10  apply (rule wf_onI2)
    1.11  apply (subgoal_tac "ALL z:A. f`z=f`y --> z: Ba")