changeset 25595 | 6c48275f9c76 |
parent 24423 | ae9cd0e92423 |
child 25885 | 6fbc3f54f819 |
--- a/src/HOL/Library/Executable_Set.thy Mon Dec 10 11:24:09 2007 +0100 +++ b/src/HOL/Library/Executable_Set.thy Mon Dec 10 11:24:12 2007 +0100 @@ -6,7 +6,7 @@ header {* Implementation of finite sets by lists *} theory Executable_Set -imports Main +imports List begin subsection {* Definitional rewrites *}