# 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";