Provided by: eprover_3.0.03+ds-1_amd64 bug

NAME

       ekb_insert - manual page for ekb_insert 3.0.03-DEBUG

SYNOPSIS

       ekb_insert [options] [names]

DESCRIPTION

       ekb_insert 3.0.03-DEBUG

       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.

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.

COPYRIGHT

       Copyright 1998-2023 by Stephan Schulz, schulz@eprover.org, and the E contributors (see DOC/CONTRIBUTORS).

       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

       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.0.03-DEBUG                           December 2023                                    EKB_INSERT(1)