author | paulson |
Tue, 23 Dec 1997 11:41:12 +0100 | |
changeset 4469 | 399868bf8444 |
parent 4468 | d17524e0beb0 |
child 4470 | af3239def3d4 |
src/HOL/Set.ML | file | annotate | diff | comparison | revisions |
--- 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";