1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
\DOC g
\TYPE {g : term -> goalstack}
\SYNOPSIS
Initializes the subgoal package with a new goal which has no assumptions.
\DESCRIBE
The call
{
g `tm`
}
\noindent is equivalent to
{
set_goal([],`tm`)
}
\noindent 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 : goalstack = 1 subgoal (1 total)
`HD [1; 2; 3] = 1 /\ TL [1; 2; 3] = [2; 3]`
}
\SEEALSO
b, e, p, r, set_goal, top_goal, top_thm.
\ENDDOC
|
