# HG changeset patch
# User paulson
# Date 882873672 -3600
# Node ID 399868bf8444451d83f9ddd68273e5de7d98c449
# Parent  d17524e0beb0668cb2e1259b5c477d963fcab246
Overloading info for image

diff -r d17524e0beb0 -r 399868bf8444 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Tue Dec 23 11:40:47 1997 +0100
+++ b/src/HOL/Set.ML	Tue Dec 23 11:41:12 1997 +0100
@@ -126,6 +126,8 @@
     ["Ball", "Bex"];
 (*need UNION, INTER also?*)
 
+(*Image: retain the type of the set being expressed*)
+Blast.overloaded ("op ``", domain_type o domain_type);
 
 (*Rule in Modus Ponens style*)
 val major::prems = goalw Set.thy [subset_def] "[| A <= B;  c:A |] ==> c:B";