author | wenzelm |
Tue, 24 Jan 2006 00:44:39 +0100 | |
changeset 18772 | f0dd51087eb3 |
parent 18771 | 63efe00371af |
child 18773 | 0eabf66582d0 |
--- a/src/HOL/Library/ExecutableSet.thy Tue Jan 24 00:43:34 2006 +0100 +++ b/src/HOL/Library/ExecutableSet.thy Tue Jan 24 00:44:39 2006 +0100 @@ -62,7 +62,7 @@ fun Ball S P = Library.forall P S; *} -code_generate "op mem" +code_generate ("op mem") code_primconst "insert" depending_on ("List.const.member")