# HG changeset patch
# User berghofe
# Date 1034252599 -7200
# Node ID 8ee6ea6627e11b808887f06d1abadfe5f1b66f13
# Parent  2b234b07924599256ca346d87f1507c6acd5ec45
Removed obsolete function "fun_rel_comp".

diff -r 2b234b079245 -r 8ee6ea6627e1 src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Thu Oct 10 14:21:49 2002 +0200
+++ b/src/HOL/Relation.ML	Thu Oct 10 14:23:19 2002 +0200
@@ -73,9 +73,6 @@
 val diag_eqI = thm "diag_eqI";
 val diag_iff = thm "diag_iff";
 val diag_subset_Times = thm "diag_subset_Times";
-val fun_rel_comp_def = thm "fun_rel_comp_def";
-val fun_rel_comp_mono = thm "fun_rel_comp_mono";
-val fun_rel_comp_unique = thm "fun_rel_comp_unique";
 val inv_image_def = thm "inv_image_def";
 val pair_in_Id_conv = thm "pair_in_Id_conv";
 val reflD = thm "reflD";
diff -r 2b234b079245 -r 8ee6ea6627e1 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Thu Oct 10 14:21:49 2002 +0200
+++ b/src/HOL/Relation.thy	Thu Oct 10 14:23:19 2002 +0200
@@ -20,9 +20,6 @@
   rel_comp  :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set"  (infixr "O" 60)
   "r O s == {(x,z). EX y. (x, y) : s & (y, z) : r}"
 
-  fun_rel_comp :: "['a => 'b, ('b * 'c) set] => ('a => 'c) set"
-  "fun_rel_comp f R == {g. ALL x. (f x, g x) : R}"
-
   Image :: "[('a * 'b) set, 'a set] => 'b set"                (infixl "``" 90)
   "r `` s == {y. EX x:s. (x,y):r}"
 
@@ -141,20 +138,6 @@
   by blast
 
 
-subsection {* Composition of function and relation *}
-
-lemma fun_rel_comp_mono: "A \<subseteq> B ==> fun_rel_comp f A \<subseteq> fun_rel_comp f B"
-  by (unfold fun_rel_comp_def) fast
-
-lemma fun_rel_comp_unique:
-  "ALL x. EX! y. (f x, y) : R ==> EX! g. g : fun_rel_comp f R"
-  apply (unfold fun_rel_comp_def)
-  apply (rule_tac a = "%x. THE y. (f x, y) : R" in ex1I)
-  apply (fast dest!: theI')
-  apply (fast intro: ext the1_equality [symmetric])
-  done
-
-
 subsection {* Reflexivity *}
 
 lemma reflI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl A r"