author | haftmann |
Thu, 24 Sep 2009 18:29:29 +0200 | |
changeset 32680 | faf6924430d9 |
parent 32679 | 096306d7391d |
child 32681 | adeac3cbb659 |
--- a/src/HOL/Library/Executable_Set.thy Thu Sep 24 18:29:29 2009 +0200 +++ b/src/HOL/Library/Executable_Set.thy Thu Sep 24 18:29:29 2009 +0200 @@ -32,9 +32,6 @@ declare inter [code] -declare Inter_image_eq [symmetric, code_unfold] -declare Union_image_eq [symmetric, code_unfold] - declare List_Set.project_def [symmetric, code_unfold] definition Inter :: "'a set set \<Rightarrow> 'a set" where