renamed Univalent to univalent
authoroheimb
Mon Feb 21 13:57:07 2000 +0100 (2000-02-21)
changeset 8268722074b93cdd
parent 8267 2ae7f9b2c0bf
child 8269 d28f549105fe
renamed Univalent to univalent
src/HOL/RelPow.ML
src/HOL/Relation.ML
src/HOL/Relation.thy
     1.1 --- a/src/HOL/RelPow.ML	Mon Feb 21 11:16:19 2000 +0100
     1.2 +++ b/src/HOL/RelPow.ML	Mon Feb 21 13:57:07 2000 +0100
     1.3 @@ -105,12 +105,12 @@
     1.4  qed "rtrancl_is_UN_rel_pow";
     1.5  
     1.6  
     1.7 -Goal "!!r::('a * 'a)set. Univalent r ==> Univalent (r^n)";
     1.8 -by (rtac UnivalentI 1);
     1.9 +Goal "!!r::('a * 'a)set. univalent r ==> univalent (r^n)";
    1.10 +by (rtac univalentI 1);
    1.11  by (induct_tac "n" 1);
    1.12   by (Simp_tac 1);
    1.13 -by (fast_tac (claset() addDs [UnivalentD] addEs [rel_pow_Suc_E]) 1);
    1.14 -qed_spec_mp "Univalent_rel_pow";
    1.15 +by (fast_tac (claset() addDs [univalentD] addEs [rel_pow_Suc_E]) 1);
    1.16 +qed_spec_mp "univalent_rel_pow";
    1.17  
    1.18  
    1.19  
     2.1 --- a/src/HOL/Relation.ML	Mon Feb 21 11:16:19 2000 +0100
     2.2 +++ b/src/HOL/Relation.ML	Mon Feb 21 13:57:07 2000 +0100
     2.3 @@ -398,17 +398,17 @@
     2.4  by (Blast_tac 1);
     2.5  qed "Image_subset_eq";
     2.6  
     2.7 -section "Univalent";
     2.8 +section "univalent";
     2.9  
    2.10 -Goalw [Univalent_def]
    2.11 -     "!x y. (x,y):r --> (!z. (x,z):r --> y=z) ==> Univalent r";
    2.12 +Goalw [univalent_def]
    2.13 +     "!x y. (x,y):r --> (!z. (x,z):r --> y=z) ==> univalent r";
    2.14  by (assume_tac 1);
    2.15 -qed "UnivalentI";
    2.16 +qed "univalentI";
    2.17  
    2.18 -Goalw [Univalent_def]
    2.19 -     "[| Univalent r;  (x,y):r;  (x,z):r|] ==> y=z";
    2.20 +Goalw [univalent_def]
    2.21 +     "[| univalent r;  (x,y):r;  (x,z):r|] ==> y=z";
    2.22  by Auto_tac;
    2.23 -qed "UnivalentD";
    2.24 +qed "univalentD";
    2.25  
    2.26  
    2.27  (** Graphs of partial functions **)
     3.1 --- a/src/HOL/Relation.thy	Mon Feb 21 11:16:19 2000 +0100
     3.2 +++ b/src/HOL/Relation.thy	Mon Feb 21 13:57:07 2000 +0100
     3.3 @@ -40,8 +40,8 @@
     3.4    trans  :: "('a * 'a)set => bool"          (*transitivity predicate*)
     3.5      "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)"
     3.6  
     3.7 -  Univalent :: "('a * 'b)set => bool"
     3.8 -    "Univalent r == !x y. (x,y):r --> (!z. (x,z):r --> y=z)"
     3.9 +  univalent :: "('a * 'b)set => bool"
    3.10 +    "univalent r == !x y. (x,y):r --> (!z. (x,z):r --> y=z)"
    3.11  
    3.12    fun_rel_comp :: "['a => 'b, ('b * 'c) set] => ('a => 'c) set"
    3.13      "fun_rel_comp f R == {g. !x. (f x, g x) : R}"