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

NAME

6       ekb_insert - manual page for ekb_insert 2.3-DEBUG
7

SYNOPSIS

9       ekb_insert [options] [names]
10

DESCRIPTION

12       ekb_insert 2.3-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 © 1999-2012 by Stephan Schulz, schulz@eprover.org
71
72       This  program  is  a part of the support structure for the E equational
73       theorem prover. You can find the latest version of the  E  distribution
74       as well as additional information at http://www.eprover.org
75
76       This program is free software; you can redistribute it and/or modify it
77       under the terms of the GNU General Public License as published  by  the
78       Free  Software Foundation; either version 2 of the License, or (at your
79       option) any later version.
80
81       This program is distributed in the hope that it  will  be  useful,  but
82       WITHOUT  ANY  WARRANTY;  without  even  the  implied  warranty  of MER‐
83       CHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU  General
84       Public License for more details.
85
86       You should have received a copy of the GNU General Public License along
87       with this program (it should be contained in the top level directory of
88       the  distribution in the file COPYING); if not, write to the Free Soft‐
89       ware  Foundation,  Inc.,  59  Temple  Place,  Suite  330,  Boston,   MA
90       02111-1307 USA
91
92       The original copyright holder can be contacted as
93
94       Stephan  Schulz  Technische Universitaet Muenchen Fakultaet fuer Infor‐
95       matik Arcisstrasse 20 D-80290 Muenchen Germany
96
97
98
99ekb_insert 2.3-DEBUG              April 2019                     EKB_INSERT(1)
Impressum