(10steps 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: decidable divides 1
1. a : 
2. b : 
  Dec(a | b)
By: Decide (a = 0)

Generated subgoals:

1 3. a = 0
  Dec(a | b)
4 steps
2 3. a = 0
  Dec(a | b)
4 steps

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

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