Overloading info for image
authorpaulson
Tue Dec 23 11:41:12 1997 +0100 (1997-12-23)
changeset 4469399868bf8444
parent 4468 d17524e0beb0
child 4470 af3239def3d4
Overloading info for image
src/HOL/Set.ML
     1.1 --- a/src/HOL/Set.ML	Tue Dec 23 11:40:47 1997 +0100
     1.2 +++ b/src/HOL/Set.ML	Tue Dec 23 11:41:12 1997 +0100
     1.3 @@ -126,6 +126,8 @@
     1.4      ["Ball", "Bex"];
     1.5  (*need UNION, INTER also?*)
     1.6  
     1.7 +(*Image: retain the type of the set being expressed*)
     1.8 +Blast.overloaded ("op ``", domain_type o domain_type);
     1.9  
    1.10  (*Rule in Modus Ponens style*)
    1.11  val major::prems = goalw Set.thy [subset_def] "[| A <= B;  c:A |] ==> c:B";