summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | berghofe |

Wed, 07 May 2008 10:59:33 +0200 | |

changeset 26818 | b4a24433154e |

parent 26817 | 9217577e0a23 |

child 26819 | 56036226028b |

Instantiated rule expand_fun_eq in proof of set_of_eq_empty_iff, to avoid that
it gets applied to sets as well.

--- a/src/HOL/Library/Multiset.thy Wed May 07 10:59:32 2008 +0200 +++ b/src/HOL/Library/Multiset.thy Wed May 07 10:59:33 2008 +0200 @@ -196,7 +196,7 @@ by (auto simp add: set_of_def) lemma set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})" -by (auto simp: set_of_def Mempty_def in_multiset count_def expand_fun_eq) +by (auto simp: set_of_def Mempty_def in_multiset count_def expand_fun_eq [where f="Rep_multiset M"]) lemma mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)" by (auto simp add: set_of_def)