Mark muliple-goal commands as experimental (#471)

Due to issue #316.

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

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'." ]