| changeset 5336 | 721bf1a13f1a |
| parent 5318 | 72bf8039b53f |
| child 5450 | fe9d103464a4 |
--- a/src/HOL/Set.ML Wed Aug 19 10:27:00 1998 +0200 +++ b/src/HOL/Set.ML Wed Aug 19 10:27:25 1998 +0200 @@ -125,7 +125,7 @@ (*need UNION, INTER also?*) (*Image: retain the type of the set being expressed*) -Blast.overloaded ("op ``", domain_type o domain_type); +Blast.overloaded ("op ``", domain_type); (*Rule in Modus Ponens style*) Goalw [subset_def] "[| A <= B; c:A |] ==> c:B";