1 files changed, 4 insertions, 8 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index de1fdb00..16b988c9 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -1856,14 +1856,6 @@ namespace Microsoft.Boogie {
       one of them to keep; otherwise, Boogie ignore the :extern declaration
       and keeps the other.
 
-  ---- On axioms -------------------------------------------------------------
-
-    {:inline true}
-      Works on axiom of the form:
-        (forall VARS :: f(VARS) = expr(VARS))
-      Makes Boogie replace f(VARS) with expr(VARS) everywhere just before
-      doing VC generation.
-
   ---- On implementations and procedures -------------------------------------
 
      {:inline N}
@@ -1897,6 +1889,10 @@ namespace Microsoft.Boogie {
      {:bvbuiltin ""spec""}
        Rewrite the function to built-in prover function symbol 'fn'.
 
+     {:inline}
+     {:inline true}
+       Expand function according to its definition before going to the prover.
+
      {:never_pattern true}
        Terms starting with this function symbol will never be
        automatically selected as patterns. It does not prevent them