More permissive use of @extern without library so that the body is compiled...

More permissive use of @extern without library so that the body is compiled but not directly executable.

library/lazy/package.scala

@@ -22,10 +22,10 @@ object $ {
    * Should be used only in ensuring.
    * TODO: enforce this.
    */
-  @extern @library
+  @extern
   def inState[T] : Set[$[T]] = sys.error("inState method is not executable!")
 
-  @extern @library
+  @extern
   def outState[T] : Set[$[T]] = sys.error("outState method is not executable")
 
   /**

src/main/scala/leon/codegen/CodeGeneration.scala

@@ -201,7 +201,7 @@ trait CodeGeneration {
       funDef.fullBody
     } else {
       funDef.body.getOrElse(
-        if(funDef.annotations contains "library") {
+        if(funDef.annotations contains "extern") {
           Error(funDef.id.getType, "Body of " + funDef.id.name + " not implemented at compile-time and still executed.")
         } else {
           throw CompilationException("Can't compile a FunDef without body: "+funDef.id.name)