g : term quotation -> proofs

- STRUCTURE
- SYNOPSIS
- Initializes the subgoal package with a new goal which has no assumptions.
- DESCRIPTION
- The callis equivalent to
g `tm`

and clearly more convenient if a goal has no assumptions. For a description of the subgoal package, see set_goal.set_goal([],Term`tm`)

- 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: 1 proof. 1. Incomplete: Initial goal: (HD [1; 2; 3] = 1) /\ (TL [1; 2; 3] = [2; 3]) : GoalstackPure.proofs

- SEEALSO

HOL Trindemossen-1