diff --git a/doc/manual/manual.md b/doc/manual/manual.md
index 23c9b9cd70..1f9631d7b7 100644
--- a/doc/manual/manual.md
+++ b/doc/manual/manual.md
@@ -1246,7 +1246,8 @@ immediately returns `True`). It fails if that is not the case.
 The proof scripts shown so far all have a single implicit goal. As in
 many other interactive provers, however, SAWScript proofs can have
 multiple goals. The following commands can introduce or work with
-multiple goals.
+multiple goals. These are experimental and can be used only after
+`enable_experimental` has been called.
 
 * `goal_apply : Theorem -> ProofScript ()` will apply a given
 introduction rule to the current goal. This will result in zero or more
diff --git a/doc/manual/manual.pdf b/doc/manual/manual.pdf
index 6ede224850..dcfec8152e 100644
Binary files a/doc/manual/manual.pdf and b/doc/manual/manual.pdf differ
diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index e78e1b112b..ff55281736 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/src/SAWScript/Interpreter.hs
@@ -1000,30 +1000,30 @@ primitives = Map.fromList
 
   , prim "goal_apply"          "Theorem -> ProofScript ()"
     (pureVal goal_apply)
-    Current
+    Experimental
     [ "Apply an introduction rule to the current goal. Depending on the"
     , "rule, this will result in zero or more new subgoals."
     ]
   , prim "goal_assume"         "ProofScript Theorem"
     (pureVal goal_assume)
-    Current
+    Experimental
     [ "Convert the first hypothesis in the current proof goal into a"
     , "local Theorem."
     ]
   , prim "goal_insert"         "Theorem -> ProofScript ()"
     (pureVal goal_insert)
-    Current
+    Experimental
     [ "Insert a Theorem as a new hypothesis in the current proof goal."
     ]
   , prim "goal_intro"          "String -> ProofScript Term"
     (pureVal goal_intro)
-    Current
+    Experimental
     [ "Introduce a quantified variable in the current proof goal, returning"
     , "the variable as a Term."
     ]
   , prim "goal_when"           "String -> ProofScript () -> ProofScript ()"
     (pureVal goal_when)
-    Current
+    Experimental
     [ "Run the given proof script only when the goal name contains"
     , "the given string."
     ]
@@ -1188,7 +1188,7 @@ primitives = Map.fromList
 
   , prim "split_goal"          "ProofScript ()"
     (pureVal split_goal)
-    Current
+    Experimental
     [ "Split a goal of the form 'Prelude.and prop1 prop2' into two separate"
     ,  "goals 'prop1' and 'prop2'." ]