g : term -> goalstack

SYNOPSIS

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

DESCRIPTION

The call

   g `tm`

is equivalent to

   set_goal([],`tm`)

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

FAILURE CONDITIONS

Fails unless the argument term has type bool.

EXAMPLE

  # g `HD[1;2;3] = 1 /\ TL[1;2;3] = [2;3]`;;
  val it : goalstack = 1 subgoal (1 total)

  `HD [1; 2; 3] = 1 /\ TL [1; 2; 3] = [2; 3]`

SEE ALSO

b, e, p, r, set_goal, top_goal, top_thm.