# HG changeset patch # User wenzelm # Date 1138059879 -3600 # Node ID f0dd51087eb3315c7524f327fb4e946c4c5c1b44 # Parent 63efe00371afe45f0de32f6c79961de7e3ec0feb fixed code_generate syntax; diff -r 63efe00371af -r f0dd51087eb3 src/HOL/Library/ExecutableSet.thy --- 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")