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