Library Editing

view  obname

The object obname is displayed in a new window. If the object is not already being viewed the new view will be fully editable; otherwise, it and all other views of the object will be made read-only  . The header line of the view will say SHOW  for a read-only view and EDIT  for an editable view.

The editor used depends on the kind of object. The proof editor  is used on theorem objects, while the term editor is used for all other objects. For more information on the proof editor see Section and on the term editor, see Section

If view  is used on a theorem object with an compressed proof, expansion of the proof is forced. This may take some time, especially if the proof is large.

create_rule obname place
create_thm obname place
create_abs obname place
create_ml obname place
create_disp obname place
create_com obname place
create_lat obname place

Create new objects of the appropriate kind with name obname, and position it before object place.

Rename object old-obname to new-obname.

delete  obname

Delete object obname from the library.

delete_objects from-obname to-obname

Delete the range of objects from from-obname to object to-obname inclusive.

check  obname

Check object obname. If necessary, the library window is redisplayed to show the object's new status.

Checking a rule, abstraction, precedence or display form object causes the object's contents to be verified. See Section ??? for a description of what verification involves. If the object is well-formed, it is incorporated into the Nuprl environment.

When is checking necessary??? After all one always checks on loading and exiting an object...

Checking an ML object invokes the ML reader on the object's contents.

Checking a theorem object, forcesexpansion  of its proof, if the proof was initially compressed. Note that this might take a while. See Section for details.

What is effect on extraction???

Checking a comment object has no effect, other than to change the status of a raw comment object to complete.

check_objects from-obname to-obname 

Check from object from-obname to object to-obname inclusive. Stop if the status of any object changes on checking. This prevents a cascade of further status changes which might be caused by this status change.

move  obname place

Move object obname before object place.

move_objects from-obname to-obname place 

Move the range of objects from from-obname to object to-obname inclusive to immediately before object place.