next up previous contents
Next: Entering the Main Goal Up: The Nuprl Proof Development Previous: Printing a Theory

Creating a Theorem

Create a theorem object. Enter:





\begin{parbox} {25em} {\tt create\_thm {\tt \char `\uml }{}not\_over\_and{\tt \c... ...x{ \framebox {\rule[-.2ex]{0em}{1.5ex}\sc return} }\hspace{.2em}\ }\end{parbox}




The library window should now look like

Library
*C class_prop_begin *********** CLASS PROP ****************
*t dneg_elim $\forall$A:${\Bbb{P}}${i}. $\neg$$\neg$A $\Rightarrow$A
*t imp_elim $\forall$A:${\Bbb{P}}${i}. $\forall$B:${\Bbb{P}}${i}. (A $\Rightarrow$ B) $\Rightarrow$ $\neg$A $\vee$ B
*t neg_imp_elim $\forall$A:${\Bbb{P}}${i}. $\forall$B:${\Bbb{P}}${i}. $\neg$(A $\Rightarrow$ B) $\Rightarrow$ A $\wedge$ $\neg$B
*t neg_or_elim $\forall$A:${\Bbb{P}}${i}. $\forall$B:${\Bbb{P}}${i}. $\neg$(A $\vee$ B) $\Rightarrow$ $\neg$A $\wedge$ $\neg$B
*t neg_and_elim $\forall$A:${\Bbb{P}}${i}. $\forall$B:${\Bbb{P}}${i}. $\neg$(A $\wedge$ B) $\Rightarrow$ $\neg$A $\vee$ $\neg$B
*t pierce $\forall$P:${\Bbb{P}}${i}. $\forall$Q:${\Bbb{P}}${i}. ((P $\Rightarrow$ Q) $\Rightarrow$ P) $\Rightarrow$ P
*C class_prop_end ***************************************
*C user_begin ************** USER *****************
?t not_over_and [term]
*C user_end *************************************
 

View the theorem. Enter:





\begin{parbox} {25em} {\tt view {\tt \char `\uml }{}not\_over\_and{\tt \char `\u... ...x{ \framebox {\rule[-.2ex]{0em}{1.5ex}\sc return} }\hspace{.2em}\ }\end{parbox}




Nuprl opens up a proof editor window. The window should appear as:

EDIT THM not_over_and
? top
<main proof goal>
 
 
 
 
 

Move the mouse cursor over into the new window, and click \framebox {\rule[-.2ex]{0em}{1.5ex}\sc mouse-left} . The cursor in the ML-Top-Loopwindow vanishes, and a new cursor appears in the proof window. In general, \framebox {\rule[-.2ex]{0em}{1.5ex}\sc mouse-left} can be used to switch to different Nuprl windows. Only one window at a time has a cursor. The window with the cursor receives the input from keyboard strokes and mouse clicks. Often but not always, this window is the same as the window containing the mouse; there are a couple of keyboard commands which move the cursor between windows without moving the mouse.

To Exit a proof window, use $\langle$C-Z$\rangle$. This saves the proof and closes the window.

next up previous contents
Next: Entering the Main Goal Up: The Nuprl Proof Development Previous: Printing a Theory
Dora Abdullah, 12/4/97