res_quan/Manual/summary.tex

5 \title{Summary of the {\tt res\_quan} library}
16 {\tt res\_quan}, which  contains a number of theorems about the
18 for dealing with them. This summary lists all theorem stored in the
19 {\tt res\_quan} theory and ML functions available in the library.
23 This theory caontains the following theorems.
51 % \ENDTHEOREM just finishes off the group (and kick page if necessary)
99 \section{ML functions in the library}
184 Generalizes the conclusion of a theorem to a restricted universal quantification.
188 in the conclusion of a theorem.
191 Generalizes the conclusion of a theorem over its own assumptions.
194 Strip a restricted existential quantification in the conclusion of a theorem.
197 Strip a restricted universal quantification in the conclusion of a theorem.
206 Specializes the conclusion of a restricted universally quantified theorem.
209 Specializes zero or more variables in the conclusion of a restricted
213 Specializes the conclusion of a theorem with its own quantified variables.
238 Changes the order of two restricted universal quantifications.
248 Strips the outermost restricted universal quantifier from
249 the conclusion of a goal.
252 Strips the outermost restricted universal quantifier from
253 the conclusion of a goal.
256 Strips the outermost restricted extistential quantifier from
257 the conclusion of a goal.
261 the assumptions of a goal.
265 the assumptions of a goal.
269 quantifications in them against the others.
283 Declare a new binder and install a definitional axiom in the current theory.
286 Declare a new infix constant and install a definitional axiom in the current theory.
289 Declare a new constant and install a definitional axiom in the current theory.