ekb_insert - Man Page
manual page for ekb_insert 3.1.0-DEBUG
Synopsis
ekb_insert [options] [names]
Description
ekb_insert 3.1.0-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-2024 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