
# Copyright (c) 2012 United States Government as represented by
# the National Aeronautics and Space Administration.  No copyright
# is claimed in the United States under Title 17, U.S.Code. All Other
# Rights Reserved.
#
# The software in this package has been released as open-source software
# under the NASA Open Source Agreement.  See the accompanying file
# NASA_Open_Source_Agreement.pdf for a full description of the terms.


quick_text = '''
PVS Client for Hypatheon			Version %s


<:topic::Quick Start Guide:>


Enter search terms and press <:bold::Search:> to query the <:bold::Hypatheon database:>.

Types of query terms:

	- <:bold::Name::> one or more name fragments to match candidate <:bold::declaration names:>
	- <:bold::Refs::> one or more name fragments to match <:bold::functions referenced:> by candidate lemmas

Select items in listboxes to display full declarations and their theories.

Choose one of the <:bold::prover command buttons:> (Lem, Use, Rew) to invoke the corresponding command in the PVS prover buffer.

Right-clickable <:bold::context menus:> are available for each query result item displayed.

Select the <:topic::User's Guide:> from the Help menu for a full description of all features.


<:topic::Example:>

A search using the Name terms 'expt pos gt' finds these 5 lemmas:

both_sides_expt_pos_gt_aux
pos_expt_gt
both_sides_expt_pos_gt
expt_gt1_pos
expt_gt1_nonpos
'''
