author | paulson |
Wed, 19 Aug 1998 10:27:25 +0200 | |
changeset 5336 | 721bf1a13f1a |
parent 5335 | 07fb8999de62 |
child 5337 | 2f7d09a927c4 |
src/HOL/Set.ML | file | annotate | diff | comparison | revisions |
--- 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";