next up previous contents
Next: Theorem Export Commands Up: Appendix: Reference for Individual Previous: Environment Desktop Commands

View Management Commands

showviews
This command shows all views in a tabular format.

showview
``showview view'' shows the view ``view'' in a tabular format (translation of terms in the source theory to terms in the target theory; views are stored as part of the source theory).

viewofin
``viewofin ident view'' shows the translation of ``ident'' in the view ``view''.

clearviews
Erases all views.

dropaview
``dropaview view'' erases the view ``view''.

dropfromview
``dropfromview view ident'' drops the translation of ``ident'' from the view ``view''.

viewasselfin
``viewasselfin ident view'' causes ``ident'' to be translated by ``ident'' in view ``view''.

viewasin
``viewasin name1 name2 view'' causes ``name1'' to be translated as ``name2'' in view ``view'' (name1 must be an identifier in the current theory).

declareview
``declareview view'' creates a view with some default content.



Randall Holmes
Fri Sep 5 16:28:58 MDT 1997