g

proofManagerLib.g : term quotation -> proofs

Initializes the subgoal package with a new goal which has no assumptions.

The call

   g `tm`

is equivalent to

   set_goal([],Term`tm`)

and clearly more convenient if a goal has no assumptions. For a description of the subgoal package, see set_goal.

Failure

Fails unless the argument term has type bool.

Example

> g `(HD[1;2;3] = 1) /\ (TL[1;2;3] = [2;3])`;
val it =
   Proof manager status: 3 proofs.
   3. Completed goalstack:  [.] ⊢ q
   
   2. Completed goalstack: ⊢ HD [1; 2; 3] = 1 ∧ TL [1; 2; 3] = [2; 3]
   
   1. Incomplete goalstack:
        Initial goal:
        HD [1; 2; 3] = 1 ∧ TL [1; 2; 3] = [2; 3]

See also

proofManagerLib.set_goal, proofManagerLib.restart, proofManagerLib.backup, proofManagerLib.redo, proofManagerLib.restore, proofManagerLib.save, proofManagerLib.set_backup, proofManagerLib.expand, proofManagerLib.expandf, proofManagerLib.p, proofManagerLib.top_thm, proofManagerLib.top_goal