changeset 4469 | 399868bf8444 |
parent 4434 | 75f38104ff80 |
child 4477 | b3e5857d8d99 |
--- 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";