equal
deleted
inserted
replaced
133 |
133 |
134 overload_1st_set "Ball"; (*need UNION, INTER also?*) |
134 overload_1st_set "Ball"; (*need UNION, INTER also?*) |
135 overload_1st_set "Bex"; |
135 overload_1st_set "Bex"; |
136 |
136 |
137 (*Image: retain the type of the set being expressed*) |
137 (*Image: retain the type of the set being expressed*) |
138 Blast.overloaded ("op ``", domain_type); |
138 Blast.overloaded ("image", domain_type); |
139 |
139 |
140 (*Rule in Modus Ponens style*) |
140 (*Rule in Modus Ponens style*) |
141 Goalw [subset_def] "[| A <= B; c:A |] ==> c:B"; |
141 Goalw [subset_def] "[| A <= B; c:A |] ==> c:B"; |
142 by (Blast_tac 1); |
142 by (Blast_tac 1); |
143 qed "subsetD"; |
143 qed "subsetD"; |