File: current_goalstack.doc

package info (click to toggle)
hol-light 20230128-1
  • links: PTS, VCS
  • area: main
  • in suites: bookworm
  • size: 45,636 kB
  • sloc: ml: 688,681; cpp: 439; makefile: 302; lisp: 286; java: 279; sh: 251; yacc: 108; perl: 78; ansic: 57; sed: 39; python: 13
file content (22 lines) | stat: -rw-r--r-- 460 bytes parent folder | download | duplicates (3) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
 
\DOC current_goalstack

\TYPE {current_goalstack : goalstack ref}

\SYNOPSIS
Reference variable holding current goalstack.

\DESCRIBE
The reference variable {current_goalstack} contains the current goalstack. A
goalstack is a type containing a list of goalstates.

\FAILURE
Not applicable.

\COMMENTS
Users will probably not often want to examine this variable explicitly, since
various proof commands modify it in various ways.

\SEEALSO
b, g, e, r.

\ENDDOC