# HG changeset patch
# User paulson
# Date 942312254 -3600
# Node ID 6273f58ea2c102a4445da204086737318db112a8
# Parent  5244d7ed31b919994a04bc5783b7ecce97fbd42a
Fixed obsolete use of "op ^^"; new lemma

diff -r 5244d7ed31b9 -r 6273f58ea2c1 src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Sat Nov 06 15:34:12 1999 +0100
+++ b/src/HOL/Relation.ML	Thu Nov 11 10:24:14 1999 +0100
@@ -309,7 +309,7 @@
 
 (*** Image of a set under a relation ***)
 
-overload_1st_set "Relation.op ^^";
+overload_1st_set "Relation.Image";
 
 Goalw [Image_def] "b : r^^A = (? x:A. (x,b):r)";
 by (Blast_tac 1);
@@ -389,6 +389,9 @@
 by (Blast_tac 1);
 qed "Image_INT_subset";
 
+Goal "(r^^A <= B) = (A <= - ((r^-1) ^^ (-B)))";
+by (Blast_tac 1);
+qed "Image_subset_eq";
 
 section "Univalent";