ekb_insert - manual page for ekb_insert 3.2.5

Copyright

This program is a part of the distribution of the equational theorem prover E. You can find the latest
version of the E distribution as well as additional information at http://www.eprover.org

This program is free software; you can redistribute it and/or modify it under the terms of the GNU
General Public License as published by the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even
the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
License for more details.

You should have received a copy of the GNU General Public License along with this program (it should be
contained in the top level directory of the distribution in the file COPYING); if not, write to the Free
Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA

We welcome bug reports and even reasonable questions. If the prover behaves in an unexpected way, please
include the following information:

- What did you observe? - What did you expect? - The output of `eprover --version` - The full
commandline that lead to the unexpected behaviour - The input file(s) that lead to the unexpected
behaviour

Most bug reports should be send to <schulz@eprover.org>. Bug reports with respect to the HO-version
should be send to or at least copied to <jasmin.blanchette@gmail.com>. Please remember that this is an
unpaid volunteer service.

The original copyright holder can be contacted via email or as

Stephan Schulz DHBW Stuttgart Fakultaet Technik Informatik Lerchenstrasse 1 70174 Stuttgart Germany

ekb_insert 3.2.5 October 2024 EKB_INSERT(1)

Description

       ekb_insert 3.2.5

       Insert  example  files into an E knowledge base. Each non-option argument is considered as one individual
       example file. For most applications this is obsolete, use ekb_ginsert instead.

       Options

       -h--help

              Print a short description of program usage and options.

       -V--version

              Print the version number of the program.

       -v--verbose[=<arg>]

              Verbose comments on the progress of the program. The short form  or  the  long  form  without  the
              optional argument is equivalent to --verbose=1.

       -n <arg>

       --name=<arg>

              Give  the name of the new problem. If not given, the program will take the name of the first input
              file, or, if <stdin> is read, a name of the form '__problem__i', where  i  is  magically  computed
              from the existing knowledge base.

       -k <arg>

       --knowledge-base=<arg>

              Select the knowledge base. If not given, select E_KNOWLEDGE.

Name

       ekb_insert - manual page for ekb_insert 3.2.5

Reporting Bugs

       Report bugs to <schulz@eprover.org>. Please include the following, if possible:

       * The version of the package as reported by eprover--version.

       * The operating system and version.

       * The exact command line that leads to the unexpected behaviour.

       * A description of what you expected and what actually happened.

       * If possible all input files necessary to reproduce the bug.