File: current_goalstack.doc

package info (click to toggle)
hol-light 20131026-1
  • links: PTS, VCS
  • area: main
  • in suites: jessie, jessie-kfreebsd
  • size: 26,264 kB
  • ctags: 4,620
  • sloc: ml: 400,325; cpp: 438; java: 279; lisp: 261; makefile: 256; sh: 190; yacc: 108; perl: 78; ansic: 57; sed: 39
file content (22 lines) | stat: -rw-r--r-- 462 bytes parent folder | download | duplicates (4) 
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