It is argued that Ginsberg's Possible Worlds Approach to counterfactual implication suffers from a number of defects which are the result of confusing proof theory and model theory. In particular, logically equivalent theories do not have identical counterfactual consequences, and monotonic theory revisions are not always preferred to nonmonotonic ones. This paper develops a situation semantics for counterfactual implication in which propositions are treated as operations on sets of possible worlds. Logically equivalent theories have identical consequences in the model theory, which always prefers monotonic revisions to nonmonotonic ones and validates all the axioms and derivation rules of counterfactual logic. The semantics is also contrasted with Winslett's Possible Models Approach.