1EKB_INSERT(1)                    User Commands                   EKB_INSERT(1)
2
3
4

NAME

6       ekb_insert - manual page for ekb_insert 2.6-DEBUG
7

SYNOPSIS

9       ekb_insert [options] [names]
10

DESCRIPTION

12       ekb_insert 2.6-DEBUG
13
14       Insert example files into an E knowledge base. Each non-option argument
15       is considered as one individual example  file.  For  most  applications
16       this is obsolete, use ekb_ginsert instead.
17
18       Options
19
20       -h
21
22       --help
23
24              Print a short description of program usage and options.
25
26       -V
27
28       --version
29
30              Print the version number of the program.
31
32       -v
33
34       --verbose[=<arg>]
35
36              Verbose  comments on the progress of the program. The short form
37              or the long form without the optional argument is equivalent  to
38              --verbose=1.
39
40       -n <arg>
41
42       --name=<arg>
43
44              Give the name of the new problem. If not given, the program will
45              take the name of the first input file, or, if <stdin> is read, a
46              name  of  the form '__problem__i', where i is magically computed
47              from the existing knowledge base.
48
49       -k <arg>
50
51       --knowledge-base=<arg>
52
53              Select the knowledge base. If not given, select E_KNOWLEDGE.
54

REPORTING BUGS

56       Report bugs to <schulz@eprover.org>. Please include the  following,  if
57       possible:
58
59       * The version of the package as reported by eprover --version.
60
61       * The operating system and version.
62
63       * The exact command line that leads to the unexpected behaviour.
64
65       * A description of what you expected and what actually happend.
66
67       * If possible all input files necessary to reproduce the bug.
68

70       Copyright  1998-2021  by  Stephan Schulz, schulz@eprover.org, and the E
71       contributors (see DOC/CONTRIBUTORS).
72
73       This program is a part of the distribution of  the  equational  theorem
74       prover E. You can find the latest version of the E distribution as well
75       as additional information at http://www.eprover.org
76
77       This program is free software; you can redistribute it and/or modify it
78       under  the  terms of the GNU General Public License as published by the
79       Free Software Foundation; either version 2 of the License, or (at  your
80       option) any later version.
81
82       This  program  is  distributed  in the hope that it will be useful, but
83       WITHOUT ANY  WARRANTY;  without  even  the  implied  warranty  of  MER‐
84       CHANTABILITY  or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
85       Public License for more details.
86
87       You should have received a copy of the GNU General Public License along
88       with this program (it should be contained in the top level directory of
89       the distribution in the file COPYING); if not, write to the Free  Soft‐
90       ware   Foundation,  Inc.,  59  Temple  Place,  Suite  330,  Boston,  MA
91       02111-1307 USA
92
93       The original copyright holder can be contacted via email or as
94
95       Stephan  Schulz  DHBW  Stuttgart  Fakultaet  Technik  Informatik  Rote‐
96       buehlplatz 41 70178 Stuttgart Germany
97
98
99
100ekb_insert 2.6-DEBUG             January 2023                    EKB_INSERT(1)
Impressum