ekb_insert

EKB_INSERT(1)                    User Commands                   EKB_INSERT(1)



NAME
       ekb_insert - manual page for ekb_insert 1.9

SYNOPSIS
       ekb_insert [options] [names]

DESCRIPTION
       ekb_insert 1.9

       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 happend.

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

COPYRIGHT
       Copyright © 1999-2012 by Stephan Schulz, schulz@eprover.org

       This program is a part of the support structure for the E equational
       theorem prover. 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 as

       Stephan Schulz Technische Universitaet Muenchen Fakultaet fuer
       Informatik Arcisstrasse 20 D-80290 Muenchen Germany



ekb_insert 1.9                     July 2015                     EKB_INSERT(1)