| changeset 45231 | d85a2fdc586c |
| parent 45186 | 645c6cac779e |
| child 45975 | 5e78c499a7ff |
--- a/src/HOL/Library/Executable_Set.thy Fri Oct 21 11:17:12 2011 +0200 +++ b/src/HOL/Library/Executable_Set.thy Fri Oct 21 11:17:14 2011 +0200 @@ -67,7 +67,7 @@ "{} = empty" by simp -lemma [code_unfold, code_inline del]: +lemma "empty = Set []" by simp -- {* Otherwise @{text \<eta>}-expansion produces funny things. *}