(4steps total) PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: gcd p eq args
  a:. GCD(a;a;a)
By: Unfold `gcd_p` 0 THEN GenUnivCD

Generated subgoals:

1 1. a : 
  a | a
1 step
2 1. a : 
  a | a
1 step
3 1. a : 
2. z : 
3. z | a & z | a
  z | a
Auto

About:
intall
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

(4steps total) PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Search Doc