AC_MSG_RESULT($DBHOST)
AC_SUBST(CAMLP4O)
-AC_SUBST(DISTRIBUTED)
AC_SUBST(DBHOST)
AC_SUBST(DEBUG)
-AC_SUBST(TRANSFORMER_MODULE)
-AC_SUBST(FINDLIB_REQUIRES)
+AC_SUBST(DISTRIBUTED)
AC_SUBST(FINDLIB_CREQUIRES)
+AC_SUBST(FINDLIB_REQUIRES)
AC_SUBST(HAVE_OCAMLOPT)
AC_SUBST(LABLGLADECC)
+AC_SUBST(MATITA_VERSION)
AC_SUBST(OCAMLFIND)
AC_SUBST(OCAMLPATH)
AC_SUBST(RT_BASE_DIR)
AC_SUBST(SRCROOT)
-AC_SUBST(MATITA_VERSION)
+AC_SUBST(TRANSFORMER_MODULE)
AC_OUTPUT([
components/extlib/componentsConf.ml
matita/matita.conf.xml.build
matita/buildTimeConf.ml
matita/gtkmathview.matita.conf.xml
+ matita/dist/version.txt
Makefile.defs
])
--- /dev/null
+@MATITA_VERSION@
--- /dev/null
+
+<!-- ============= Introduction ============================== -->
+
+<sect1 id="sec_intro">
+ <title>Introduction</title>
+ <sect2 id="what">
+ <title>What is Matita?</title>
+
+ <para>
+ <application>Matita</application> is a proof assistant for ...
+ </para>
+
+ </sect2>
+</sect1>
+
- <legalnotice id="legalnotice">
- <para>
- Permission is granted to copy, distribute and/or modify this
- document under the terms of the GNU Free Documentation
- License (GFDL), Version 1.1 or any later version published
- by the Free Software Foundation with no Invariant Sections,
- no Front-Cover Texts, and no Back-Cover Texts. You can find
- a copy of the GFDL at this <ulink type="help"
- url="ghelp:fdl">link</ulink> or in the file COPYING-DOCS
- distributed with this manual.
- </para>
- <para> This manual is part of a collection of GNOME manuals
- distributed under the GFDL. If you want to distribute this
- manual separately from the collection, you can do so by
- adding a copy of the license to the manual, as described in
- section 6 of the license.
- </para>
+<para> This file is part of HELM, an Hypertextual, Electronic Library of
+ Mathematics, developed at the Computer Science Department, University of
+ Bologna, Italy. </para>
- <para>
- Many of the names used by companies to distinguish their
- products and services are claimed as trademarks. Where those
- names appear in any GNOME documentation, and the members of
- the GNOME Documentation Project are made aware of those
- trademarks, then the names are in capital letters or initial
- capital letters.
- </para>
+<para> HELM 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. </para>
- <para>
- DOCUMENT AND MODIFIED VERSIONS OF THE DOCUMENT ARE PROVIDED
- UNDER THE TERMS OF THE GNU FREE DOCUMENTATION LICENSE
- WITH THE FURTHER UNDERSTANDING THAT:
-
- <orderedlist>
- <listitem>
- <para>DOCUMENT IS PROVIDED ON AN "AS IS" BASIS,
- WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED OR
- IMPLIED, INCLUDING, WITHOUT LIMITATION, WARRANTIES
- THAT THE DOCUMENT OR MODIFIED VERSION OF THE
- DOCUMENT IS FREE OF DEFECTS MERCHANTABLE, FIT FOR
- A PARTICULAR PURPOSE OR NON-INFRINGING. THE ENTIRE
- RISK AS TO THE QUALITY, ACCURACY, AND PERFORMANCE
- OF THE DOCUMENT OR MODIFIED VERSION OF THE
- DOCUMENT IS WITH YOU. SHOULD ANY DOCUMENT OR
- MODIFIED VERSION PROVE DEFECTIVE IN ANY RESPECT,
- YOU (NOT THE INITIAL WRITER, AUTHOR OR ANY
- CONTRIBUTOR) ASSUME THE COST OF ANY NECESSARY
- SERVICING, REPAIR OR CORRECTION. THIS DISCLAIMER
- OF WARRANTY CONSTITUTES AN ESSENTIAL PART OF THIS
- LICENSE. NO USE OF ANY DOCUMENT OR MODIFIED
- VERSION OF THE DOCUMENT IS AUTHORIZED HEREUNDER
- EXCEPT UNDER THIS DISCLAIMER; AND
- </para>
- </listitem>
- <listitem>
- <para>UNDER NO CIRCUMSTANCES AND UNDER NO LEGAL
- THEORY, WHETHER IN TORT (INCLUDING NEGLIGENCE),
- CONTRACT, OR OTHERWISE, SHALL THE AUTHOR,
- INITIAL WRITER, ANY CONTRIBUTOR, OR ANY
- DISTRIBUTOR OF THE DOCUMENT OR MODIFIED VERSION
- OF THE DOCUMENT, OR ANY SUPPLIER OF ANY OF SUCH
- PARTIES, BE LIABLE TO ANY PERSON FOR ANY
- DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR
- CONSEQUENTIAL DAMAGES OF ANY CHARACTER
- INCLUDING, WITHOUT LIMITATION, DAMAGES FOR LOSS
- OF GOODWILL, WORK STOPPAGE, COMPUTER FAILURE OR
- MALFUNCTION, OR ANY AND ALL OTHER DAMAGES OR
- LOSSES ARISING OUT OF OR RELATING TO USE OF THE
- DOCUMENT AND MODIFIED VERSIONS OF THE DOCUMENT,
- EVEN IF SUCH PARTY SHALL HAVE BEEN INFORMED OF
- THE POSSIBILITY OF SUCH DAMAGES.
- </para>
- </listitem>
- </orderedlist>
- </para>
- </legalnotice>
+<para> HELM 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. </para>
+<para> You should have received a copy of the GNU General Public License
+ along with HELM; if not, write to the Free Software Foundation, Inc., 59
+ Temple Place - Suite 330, Boston, MA 02111-1307, USA. A copy of the GNU
+ General Public License is available at <ulink type="help"
+ url="ghelp:gpl">this link</ulink>. </para>
<?xml version="1.0"?>
<!DOCTYPE article PUBLIC "-//OASIS//DTD DocBook XML V4.1.2//EN"
"http://www.oasis-open.org/docbook/xml/4.1.2/docbookx.dtd" [
- <!ENTITY legal SYSTEM "legal.xml">
- <!ENTITY appversion "0.0">
- <!ENTITY manrevision "0.0">
+
+ <!ENTITY license SYSTEM "legal.xml">
+ <!ENTITY intro SYSTEM "intro.xml">
+ <!ENTITY terms SYSTEM "terms.xml">
+ <!ENTITY tactics SYSTEM "tactics.xml">
+
+ <!ENTITY manrevision "0">
<!ENTITY date "February 2006">
<!ENTITY app "<application>Matita</application>">
<!ENTITY appname "Matita">
- <!ENTITY version "0.0">
+ <!ENTITY appversion SYSTEM "../../dist/version.txt">
]>
<!-- =============Document Header ============================= -->
<!-- please do not change the id; for translations, change lang to -->
<!-- appropriate code -->
<articleinfo>
- <title>&app; Manual V&manrevision;</title>
+ <title>&app; V&appversion; Manual (rev. &manrevision;)</title>
<copyright>
<year>2006</year>
</publisher>
-->
- &legal;
- <!-- This file contains link to license for the documentation (GNU FDL), and
- other legal stuff such as "NO WARRANTY" statement. Please do not change
- any of this. -->
+ <legalnotice>
+ &license;
+ </legalnotice>
<authorgroup>
<author>
<revhistory>
<revision>
- <revnumber>&appname; Manual V&manrevision;</revnumber>
+ <revnumber>&appname; V&appversion; Manual (rev. &manrevision;)</revnumber>
<date>&date;</date>
<revdescription>
<para role="author">The HELM team
section altogether -->
<legalnotice>
<title>Feedback</title>
- <para>To report a bug or make a suggestion regarding the &app; application or
- this manual, follow the directions in the
- <ulink url="http://mowgli.cs.unibo.it/bugs"
- type="help">HELM Bugzilla Page</ulink>.
+ <para>To report a bug or make a suggestion regarding the &app;
+ application or this manual, follow the directions in the
+ <ulink url="http://bugs.mowgli.cs.unibo.it" type="help">HELM Bug
+ Tracking System Page</ulink>.
</para>
<!-- Translators may also add here feedback address for translations -->
</legalnotice>
</indexterm>
<!-- ============= Document Body ============================= -->
-<!-- ============= Introduction ============================== -->
-<sect1 id="intro">
- <title>Introduction</title>
- <sect2 id="what">
- <title>What is Matita?</title>
-
- <para>
- <application>Matita</application> is a proof assistant for ...
- </para>
-
- </sect2>
-</sect1>
-
-<!-- =========== Terms, declarations and definitions ============ -->
-<sect1 id="terms_decl_def">
- <title>Terms, definitions, declarations and proofs</title>
- <sect2 id="terms">
- <title>Terms</title>
- </sect2>
- <sect2 id="definitions">
- <title>Definitions</title>
- </sect2>
- <sect2 id="declarations">
- <title>Declarations (of inductive types)</title>
- </sect2>
- <sect2 id="proofs">
- <title>Proofs</title>
- </sect2>
-</sect1>
-
-<!-- ============ Tactics ====================== -->
-<sect1 id="tactics">
- <title>Tactics</title>
-
- <sect2 id="tac_absurd">
- <title>absurd <term></title>
- <para>The tactic <command>absurd</command> </para>
-<para>
-<ulink url="#terms">ciao</ulink>
-</para>
- </sect2>
- <sect2 id="tac_apply">
- <title>apply <term></title>
- <para>The tactic <command>apply</command> </para>
- </sect2>
- <sect2 id="tac_assumption">
- <title>assumption</title>
- <para>The tactic <command>assumption</command> </para>
- </sect2>
- <sect2 id="tac_auto">
- <title>auto [depth=<int>] [width=<int>] [paramodulation] [full]</title>
- <para>The tactic <command>auto</command> </para>
- </sect2>
- <sect2 id="tac_clear">
- <title>clear <id></title>
- <para>The tactic <command>clear</command> </para>
- </sect2>
- <sect2 id="tac_clearbody">
- <title>clearbody <id></title>
- <para>The tactic <command>clearbody</command> </para>
- </sect2>
- <sect2 id="tac_change">
- <title>change <pattern> with <term></title>
- <para>The tactic <command>change</command> </para>
- </sect2>
- <sect2 id="tac_compare">
- <title>compare <term></title>
- <para>The tactic <command>compare</command> </para>
- </sect2>
- <sect2 id="tac_constructor">
- <title>constructor <int></title>
- <para>The tactic <command>constructor</command> </para>
- </sect2>
- <sect2 id="tac_contradiction">
- <title>contradiction</title>
- <para>The tactic <command>contradiction</command> </para>
- </sect2>
- <sect2 id="tac_cut">
- <title>cut <term> [as <id>]</title>
- <para>The tactic <command>cut</command> </para>
- </sect2>
- <sect2 id="tac_decide equality">
- <title>decide</title>
- <para>The tactic <command>decide equality</command> </para>
- </sect2>
- <sect2 id="tac_decompose">
- <title>decompose [<ident list>] <ident> [<intros_spec>]</title>
- <para>The tactic <command>decompose</command> </para>
- </sect2>
- <sect2 id="tac_discriminate">
- <title>discriminate <term></title>
- <para>The tactic <command>discriminate</command> </para>
- </sect2>
- <sect2 id="tac_elim">
- <title>elim <term> [using <term>] [<intros_spec>]</title>
- <para>The tactic <command>elim</command> </para>
- </sect2>
- <sect2 id="tac_elimType">
- <title>elimType <term> [using <term>]</title>
- <para>The tactic <command>elimType</command> </para>
- </sect2>
- <sect2 id="tac_exact">
- <title>exact <term></title>
- <para>The tactic <command>exact</command> </para>
- </sect2>
- <sect2 id="tac_exists">
- <title>exists</title>
- <para>The tactic <command>exists</command> </para>
- </sect2>
- <sect2 id="tac_fail">
- <title>fail</title>
- <para>The tactic <command>fail</command> </para>
- </sect2>
- <sect2 id="tac_fold">
- <title>fold <reduction_kind> <term> <pattern></title>
- <para>The tactic <command>fold</command> </para>
- </sect2>
- <sect2 id="tac_fourier">
- <title>fourier</title>
- <para>The tactic <command>fourier</command> </para>
- </sect2>
- <sect2 id="tac_fwd">
- <title>fwd <ident> [<ident list>]</title>
- <para>The tactic <command>fwd</command> </para>
- </sect2>
- <sect2 id="tac_generalize">
- <title>generalize <pattern> [as <id>]</title>
- <para>The tactic <command>generalize</command> </para>
- </sect2>
- <sect2 id="tac_id">
- <title>id</title>
- <para>The tactic <command>id</command> </para>
- </sect2>
- <sect2 id="tac_injection">
- <title>injection <term></title>
- <para>The tactic <command>injection</command> </para>
- </sect2>
- <sect2 id="tac_intro">
- <title>intro [<ident>]</title>
- <para>The tactic <command>intro</command> </para>
- </sect2>
- <sect2 id="tac_intros">
- <title>intros <intros_spec></title>
- <para>The tactic <command>intros</command> </para>
- </sect2>
- <sect2 id="tac_inversion">
- <title>intros <term></title>
- <para>The tactic <command>intros</command> </para>
- </sect2>
- <sect2 id="tac_lapply">
- <title>lapply [depth=<int>] <term> [to <term list] [using <ident>]</title>
- <para>The tactic <command>lapply</command> </para>
- </sect2>
- <sect2 id="tac_left">
- <title>left</title>
- <para>The tactic <command>left</command> </para>
- </sect2>
- <sect2 id="tac_letin">
- <title>letin <ident> ≝ <term></title>
- <para>The tactic <command>letin</command> </para>
- </sect2>
- <sect2 id="tac_normalize">
- <title>normalize <pattern></title>
- <para>The tactic <command>normalize</command> </para>
- </sect2>
- <sect2 id="tac_paramodulation">
- <title>paramodulation <pattern></title>
- <para>The tactic <command>paramodulation</command> </para>
- </sect2>
- <sect2 id="tac_reduce">
- <title>reduce <pattern></title>
- <para>The tactic <command>reduce</command> </para>
- </sect2>
- <sect2 id="tac_reflexivity">
- <title>reflexivity</title>
- <para>The tactic <command>reflexivity</command> </para>
- </sect2>
- <sect2 id="tac_replace">
- <title>replace <pattern> with <term></title>
- <para>The tactic <command>replace</command> </para>
- </sect2>
- <sect2 id="tac_rewrite">
- <title>rewrite {<|>} <term> <pattern></title>
- <para>The tactic <command>rewrite</command> </para>
- </sect2>
- <sect2 id="tac_right">
- <title>right</title>
- <para>The tactic <command>right</command> </para>
- </sect2>
- <sect2 id="tac_ring">
- <title>ring</title>
- <para>The tactic <command>ring</command> </para>
- </sect2>
- <sect2 id="tac_simplify">
- <title>simplify <pattern></title>
- <para>The tactic <command>simplify</command> </para>
- </sect2>
- <sect2 id="tac_split">
- <title>split</title>
- <para>The tactic <command>split</command> </para>
- </sect2>
- <sect2 id="tac_symmetry">
- <title>symmetry</title>
- <para>The tactic <command>symmetry</command> </para>
- </sect2>
- <sect2 id="tac_transitivity">
- <title>transitivity <term></title>
- <para>The tactic <command>transitivity</command> </para>
- </sect2>
- <sect2 id="tac_unfold">
- <title>unfold [<term>] <pattern></title>
- <para>The tactic <command>unfold</command> </para>
- </sect2>
- <sect2 id="tac_whd">
- <title>whd <pattern></title>
- <para>The tactic <command>whd</command> </para>
- </sect2>
-</sect1>
+&intro;
+&terms;
+&tactics;
<!-- ============= Application License ============================= -->
<sect1 id="license">
<title>License</title>
- <para>
- This program is free software; you can redistribute it and/or
- modify it under the terms of the <citetitle>GNU General Public
- License</citetitle> as published by the Free Software Foundation;
- either version 2 of the License, or (at your option) any later
- version.
- </para>
- <para>
- 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
- <citetitle>GNU General Public License</citetitle> for more details.
- </para>
- <para>
- A copy of the <citetitle>GNU General Public License</citetitle> is
- included as an appendix to the <citetitle>GNOME Users
- Guide</citetitle>. You may also obtain a copy of the
- <citetitle>GNU General Public License</citetitle> from the Free
- Software Foundation by visiting <ulink type="http"
- url="http://www.fsf.org">their Web site</ulink> or by writing to
- <address>
- Free Software Foundation, Inc.
- <street>59 Temple Place</street> - Suite 330
- <city>Boston</city>, <state>MA</state> <postcode>02111-1307</postcode>
- <country>USA</country>
- </address>
- </para>
+ &license;
</sect1>
</article>
--- /dev/null
+
+<!-- ============ Tactics ====================== -->
+<sect1 id="tactics">
+ <title>Tactics</title>
+
+ <sect2 id="tac_absurd">
+ <title>absurd <term></title>
+ <para>The tactic <command>absurd</command> </para>
+<para>
+</para>
+ </sect2>
+ <sect2 id="tac_apply">
+ <title>apply <term></title>
+ <para>The tactic <command>apply</command> </para>
+ </sect2>
+ <sect2 id="tac_assumption">
+ <title>assumption</title>
+ <para>The tactic <command>assumption</command> </para>
+ </sect2>
+ <sect2 id="tac_auto">
+ <title>auto [depth=<int>] [width=<int>] [paramodulation] [full]</title>
+ <para>The tactic <command>auto</command> </para>
+ </sect2>
+ <sect2 id="tac_clear">
+ <title>clear <id></title>
+ <para>The tactic <command>clear</command> </para>
+ </sect2>
+ <sect2 id="tac_clearbody">
+ <title>clearbody <id></title>
+ <para>The tactic <command>clearbody</command> </para>
+ </sect2>
+ <sect2 id="tac_change">
+ <title>change <pattern> with <term></title>
+ <para>The tactic <command>change</command> </para>
+ </sect2>
+ <sect2 id="tac_compare">
+ <title>compare <term></title>
+ <para>The tactic <command>compare</command> </para>
+ </sect2>
+ <sect2 id="tac_constructor">
+ <title>constructor <int></title>
+ <para>The tactic <command>constructor</command> </para>
+ </sect2>
+ <sect2 id="tac_contradiction">
+ <title>contradiction</title>
+ <para>The tactic <command>contradiction</command> </para>
+ </sect2>
+ <sect2 id="tac_cut">
+ <title>cut <term> [as <id>]</title>
+ <para>The tactic <command>cut</command> </para>
+ </sect2>
+ <sect2 id="tac_decide_equality">
+ <title>decide</title>
+ <para>The tactic <command>decide equality</command> </para>
+ </sect2>
+ <sect2 id="tac_decompose">
+ <title>decompose [<ident list>] <ident> [<intros_spec>]</title>
+ <para>The tactic <command>decompose</command> </para>
+ </sect2>
+ <sect2 id="tac_discriminate">
+ <title>discriminate <term></title>
+ <para>The tactic <command>discriminate</command> </para>
+ </sect2>
+ <sect2 id="tac_elim">
+ <title>elim <term> [using <term>] [<intros_spec>]</title>
+ <para>The tactic <command>elim</command> </para>
+ </sect2>
+ <sect2 id="tac_elimType">
+ <title>elimType <term> [using <term>]</title>
+ <para>The tactic <command>elimType</command> </para>
+ </sect2>
+ <sect2 id="tac_exact">
+ <title>exact <term></title>
+ <para>The tactic <command>exact</command> </para>
+ </sect2>
+ <sect2 id="tac_exists">
+ <title>exists</title>
+ <para>The tactic <command>exists</command> </para>
+ </sect2>
+ <sect2 id="tac_fail">
+ <title>fail</title>
+ <para>The tactic <command>fail</command> </para>
+ </sect2>
+ <sect2 id="tac_fold">
+ <title>fold <reduction_kind> <term> <pattern></title>
+ <para>The tactic <command>fold</command> </para>
+ </sect2>
+ <sect2 id="tac_fourier">
+ <title>fourier</title>
+ <para>The tactic <command>fourier</command> </para>
+ </sect2>
+ <sect2 id="tac_fwd">
+ <title>fwd <ident> [<ident list>]</title>
+ <para>The tactic <command>fwd</command> </para>
+ </sect2>
+ <sect2 id="tac_generalize">
+ <title>generalize <pattern> [as <id>]</title>
+ <para>The tactic <command>generalize</command> </para>
+ </sect2>
+ <sect2 id="tac_id">
+ <title>id</title>
+ <para>The tactic <command>id</command> </para>
+ </sect2>
+ <sect2 id="tac_injection">
+ <title>injection <term></title>
+ <para>The tactic <command>injection</command> </para>
+ </sect2>
+ <sect2 id="tac_intro">
+ <title>intro [<ident>]</title>
+ <para>The tactic <command>intro</command> </para>
+ </sect2>
+ <sect2 id="tac_intros">
+ <title>intros <intros_spec></title>
+ <para>The tactic <command>intros</command> </para>
+ </sect2>
+ <sect2 id="tac_inversion">
+ <title>intros <term></title>
+ <para>The tactic <command>intros</command> </para>
+ </sect2>
+ <sect2 id="tac_lapply">
+ <title>lapply [depth=<int>] <term> [to <term list] [using <ident>]</title>
+ <para>The tactic <command>lapply</command> </para>
+ </sect2>
+ <sect2 id="tac_left">
+ <title>left</title>
+ <para>The tactic <command>left</command> </para>
+ </sect2>
+ <sect2 id="tac_letin">
+ <title>letin <ident> ≝ <term></title>
+ <para>The tactic <command>letin</command> </para>
+ </sect2>
+ <sect2 id="tac_normalize">
+ <title>normalize <pattern></title>
+ <para>The tactic <command>normalize</command> </para>
+ </sect2>
+ <sect2 id="tac_paramodulation">
+ <title>paramodulation <pattern></title>
+ <para>The tactic <command>paramodulation</command> </para>
+ </sect2>
+ <sect2 id="tac_reduce">
+ <title>reduce <pattern></title>
+ <para>The tactic <command>reduce</command> </para>
+ </sect2>
+ <sect2 id="tac_reflexivity">
+ <title>reflexivity</title>
+ <para>The tactic <command>reflexivity</command> </para>
+ </sect2>
+ <sect2 id="tac_replace">
+ <title>replace <pattern> with <term></title>
+ <para>The tactic <command>replace</command> </para>
+ </sect2>
+ <sect2 id="tac_rewrite">
+ <title>rewrite {<|>} <term> <pattern></title>
+ <para>The tactic <command>rewrite</command> </para>
+ </sect2>
+ <sect2 id="tac_right">
+ <title>right</title>
+ <para>The tactic <command>right</command> </para>
+ </sect2>
+ <sect2 id="tac_ring">
+ <title>ring</title>
+ <para>The tactic <command>ring</command> </para>
+ </sect2>
+ <sect2 id="tac_simplify">
+ <title>simplify <pattern></title>
+ <para>The tactic <command>simplify</command> </para>
+ </sect2>
+ <sect2 id="tac_split">
+ <title>split</title>
+ <para>The tactic <command>split</command> </para>
+ </sect2>
+ <sect2 id="tac_symmetry">
+ <title>symmetry</title>
+ <para>The tactic <command>symmetry</command> </para>
+ </sect2>
+ <sect2 id="tac_transitivity">
+ <title>transitivity <term></title>
+ <para>The tactic <command>transitivity</command> </para>
+ </sect2>
+ <sect2 id="tac_unfold">
+ <title>unfold [<term>] <pattern></title>
+ <para>The tactic <command>unfold</command> </para>
+ </sect2>
+ <sect2 id="tac_whd">
+ <title>whd <pattern></title>
+ <para>The tactic <command>whd</command> </para>
+ </sect2>
+
+</sect1>
--- /dev/null
+
+<!-- =========== Terms, declarations and definitions ============ -->
+
+<sect1 id="sec_terms">
+ <title>Terms, definitions, declarations and proofs</title>
+
+ <sect2 id="terms">
+ <title>Terms</title>
+ <para> TODO </para>
+ </sect2>
+
+ <sect2 id="definitions">
+ <title>Definitions</title>
+ <para> TODO </para>
+ </sect2>
+
+ <sect2 id="declarations">
+ <title>Declarations (of inductive types)</title>
+ <para> TODO </para>
+ </sect2>
+
+ <sect2 id="proofs">
+ <title>Proofs</title>
+ <para> TODO </para>
+ </sect2>
+
+</sect1>
+
projects / helm.git / commitdiff