tweaks
authorpaulson
Wed Aug 21 15:57:24 2002 +0200 (2002-08-21)
changeset 13513b9e14471629c
parent 13512 80edb859fd24
child 13514 cc3bbaf1b8d3
tweaks
src/ZF/Constructible/Wellorderings.thy
src/ZF/Perm.thy
     1.1 --- a/src/ZF/Constructible/Wellorderings.thy	Wed Aug 21 15:57:08 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Wed Aug 21 15:57:24 2002 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4                   --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & <z,y> \<in> r))"
     1.5  
     1.6    wellordered :: "[i=>o,i,i]=>o"
     1.7 -    --{*every non-empty subset of @{text A} has an @{text r}-minimal element*}
     1.8 +    --{*linear and wellfounded on @{text A}*}
     1.9      "wellordered(M,A,r) == 
    1.10  	transitive_rel(M,A,r) & linear_rel(M,A,r) & wellfounded_on(M,A,r)"
    1.11  
     2.1 --- a/src/ZF/Perm.thy	Wed Aug 21 15:57:08 2002 +0200
     2.2 +++ b/src/ZF/Perm.thy	Wed Aug 21 15:57:24 2002 +0200
     2.3 @@ -97,9 +97,10 @@
     2.4  apply (blast dest: Pair_mem_PiD)
     2.5  done
     2.6  
     2.7 -lemma inj_apply_equality: "[| f:inj(A,B);  a:A;  b:A;  f`a=f`b |] ==> a=b"
     2.8 +lemma inj_apply_equality: "[| f:inj(A,B);  f`a=f`b;  a:A;  b:A |] ==> a=b"
     2.9  by (unfold inj_def, blast)
    2.10  
    2.11 +
    2.12  (** A function with a left inverse is an injection **)
    2.13  
    2.14  lemma f_imp_injective: "[| f: A->B;  ALL x:A. d(f`x)=x |] ==> f: inj(A,B)"