src/HOL/Set.ML
changeset 8005 b64d86018785
parent 8001 14c8843cd35b
child 8025 61dde9078e24
     1.1 --- a/src/HOL/Set.ML	Thu Nov 11 10:24:14 1999 +0100
     1.2 +++ b/src/HOL/Set.ML	Thu Nov 11 10:25:17 1999 +0100
     1.3 @@ -135,7 +135,7 @@
     1.4  overload_1st_set "Bex";
     1.5  
     1.6  (*Image: retain the type of the set being expressed*)
     1.7 -Blast.overloaded ("op ``", domain_type);
     1.8 +Blast.overloaded ("image", domain_type);
     1.9  
    1.10  (*Rule in Modus Ponens style*)
    1.11  Goalw [subset_def] "[| A <= B;  c:A |] ==> c:B";