X-Symbol is an Emacs package that allows the appearance of non-ascii symbols, such as mathematical operators and greek characters in file buffers. The non-ascii symbols have ascii representations that are stored in files, but converted to the non-ascii characters when the files are read into an emacs buffer with X-Symbol mode turned on. For example, the Specware symbol \_forall is displayed as ∀ and \_or is displayed as ∨. All the ascii representations begin with "\_". X-Symbol mode can be turned on and off by Toggling X-Symbol under Options in the Specware menu. When it is on, there is an X-Symbol menu that provides several mechanisms for entering X-Symbols. For example, the characters may be chosen directly from the menu from different categories, such as ∨ under the Operators sub-menu and ∀ under the Symbol sub-menu. This sub-menu also shows keyboard commands for the symbol. E.g., the keyboard shortcut for ∨ is c-= \/1. Alternatively, you can use the command c-, after \/. Repeated c-, commands will get you related X-Symbols. You can see all the available X-Symbols by selecting GRID of Characters under Other Commands in the X-Symbol menu.