</para>
</sect1>
- <sect1 id="tac_suppose">
- <title>suppose</title>
- <titleabbrev>suppose</titleabbrev>
- <para><userinput>suppose t(x) </userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">suppose</emphasis> &term; <emphasis role="bold"> (</emphasis> &id;
- <emphasis role="bold">) </emphasis> [ that is equivalent to &term; ]</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-condition:</term>
- <listitem>
- <para> &TODO; </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para> &TODO; </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequents to prove:</term>
- <listitem>
- <para>None.</para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
-
- <sect1 id="tac_bydone">
- <title>by done</title>
- <titleabbrev>by done</titleabbrev>
- <para><userinput>by [ t | _ ] done</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">by</emphasis> &term; <emphasis role="bold"> done </emphasis></para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-condition:</term>
- <listitem>
- <para>The term can be omitted with a "_", the running term will come found automatically. </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para>It closes the current sequent by applying <command>t</command>, taht it can be one under proof or the main proof.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequents to prove:</term>
- <listitem>
- <para>None.</para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
-
- <sect1 id="tac_weneedtoprove">
- <title> we need to prove</title>
- <titleabbrev>we need to prove</titleabbrev>
- <para><userinput>we need to prove t [(id)] [or equivalent t]</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">we need to prove</emphasis> &term; </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-condition:</term>
- <listitem>
- <para> &TODO; </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para> &TODO; </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequents to prove:</term>
- <listitem>
- <para>None.</para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
-
- <sect1 id="tac_weproceedbyinduction">
- <title> we proceed by induction</title>
- <titleabbrev>we proceed by induction</titleabbrev>
- <para><userinput>we proceed by induction on t to prove th</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">we proceed by induction on</emphasis> &term; <emphasis role="bold"> to prove </emphasis> &term; </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-condition:</term>
- <listitem>
- <para><command>t</command> must inhabit an inductive type and <command>th</command> must be an elimination principle for that inductive type.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para>It proceed on the values of <command>t</command>.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequents to prove:</term>
- <listitem>
- <para>It opens one new sequent to demonstrate.</para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
-
- <sect1 id="tac_weproceedbycases">
- <title>we proceed by cases</title>
- <titleabbrev>we proceed by cases</titleabbrev>
- <para><userinput>we proceed by cases on t to prove t</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">we proceed by cases on </emphasis> &term; <emphasis role="bold">to prove</emphasis> &term; </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-condition:</term>
- <listitem>
- <para> &TODO; </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para> &TODO; </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequents to prove:</term>
- <listitem>
- <para>None.</para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
-
<sect1 id="tac_byinduction">
- <title>by induction</title>
- <titleabbrev>by induction</titleabbrev>
+ <title>by induction hypothesis we know</title>
+ <titleabbrev>by induction hypothesis we know</titleabbrev>
<para><userinput>by induction hypothesis we know t (id)</userinput></para>
<para>
<variablelist>
<varlistentry role="tactic.synopsis">
<term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">by induction hypothesis we know</emphasis> &term; <emphasis role="bold"> (</emphasis> &id; <emphasis role="bold">)</emphasis></para>
+ <listitem><para><emphasis role="bold">by induction hypothesis we know</emphasis> &term; <emphasis role="bold"> (</emphasis> &id; <emphasis role="bold">)</emphasis></para>
</listitem>
</varlistentry>
<varlistentry>
<term>Pre-condition:</term>
<listitem>
- <para> &TODO; </para>
+ <para>To be used in a proof by induction to state the inductive
+ hypothesis.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
- <para> &TODO; </para>
+ <para> Introduces the inductive hypothesis. </para>
</listitem>
</varlistentry>
<varlistentry>
</para>
</sect1>
- <sect1 id="tac_thesisbecomes">
- <title>thesis becomes</title>
- <titleabbrev>thesis becomes</titleabbrev>
- <para><userinput>the thesis becomes t</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role ="bold">the thesis becomes</emphasis> &sterm; </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-condition:</term>
- <listitem>
- <para>Each subterm must be convertible with the term <command>t</command> disambiguate in the context of the matched subterm.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para>It replaces the subterm of the current sequent with the new term</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequence to prove:</term>
- <listitem>
- <para>None.</para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
-
<sect1 id="tac_case">
<title>case</title>
<titleabbrev>case</titleabbrev>
- <para><userinput>case id (id:t)list</userinput></para>
+ <para><userinput>case id (id1:t1) … (idn:tn)</userinput></para>
<para>
<variablelist>
<varlistentry role="tactic.synopsis">
<term>Synopsis:</term>
<listitem>
- <para><emphasis role="bold">case</emphasis> &id; <emphasis role="bold">(</emphasis> &id; <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">)</emphasis></para>
+ <para><emphasis role="bold">case</emphasis> &id; [<emphasis role="bold">(</emphasis> &id; <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">)</emphasis>] … </para>
</listitem>
</varlistentry>
<varlistentry>
<term>Pre-condition:</term>
<listitem>
- <para> &TODO; </para>
+ <para>To be used in a proof by induction or by cases to start
+ a new case</para>
</listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
- <para> &TODO; </para>
+ <para>Starts the new case <command>id</command> declaring
+ the local parameters <command>(id1:t1) … (idn:tn)</command></para>
</listitem>
</varlistentry>
<varlistentry>
<term>New sequents to prove:</term>
<listitem>
- <para>&TODO;</para>
+ <para>None</para>
</listitem>
</varlistentry>
</variablelist>
</para>
</sect1>
+ <sect1 id="tac_bydone">
+ <title>done</title>
+ <titleabbrev>done</titleabbrev>
+ <para><userinput>justification done</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para>&justification; <emphasis role="bold">done</emphasis></para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-condition:</term>
+ <listitem>
+ <para></para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It closes the current sequent given the justification.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+
+
+ <sect1 id="tac_exitselim">
+ <title>let such that</title>
+ <titleabbrev>let such that</titleabbrev>
+ <para><userinput>justification let x:t such that p (id)</userinput>
+ </para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para>&justification; <emphasis role="bold">let</emphasis> &id;
+ <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">such that</emphasis> &term;
+ <emphasis role="bold">(</emphasis> &id; <emphasis role="bold">)</emphasis></para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-condition:</term>
+ <listitem>
+ <para>
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It derives <command>∃x:t.p</command> using the
+ <command>justification</command> and then it introduces in the context
+ <command>x</command> and the hypothesis
+ <command>p</command> labelled with
+ <command>id</command>.
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequent to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+
<sect1 id="tac_obtain">
- <title>obtain/conclude</title>
- <titleabbrev>obtain/conclude</titleabbrev>
- <para><userinput>obtain H t=t [auto_params | exact t| proof | using t] done</userinput></para>
+ <title>obtain</title>
+ <titleabbrev>obtain</titleabbrev>
+ <para><userinput>obtain H t1 = t2 justification</userinput></para>
<para>
<variablelist>
<varlistentry role="tactic.synopsis">
<term>Synopsis:</term>
<listitem>
- <para>[<emphasis role="bold">obtain</emphasis> &id; | <emphasis role="bold">conclude</emphasis> &term;] <emphasis role="bold">=</emphasis> &term; [&autoparams; | <emphasis role="bold">exact</emphasis> &term; | <emphasis role="bold">using</emphasis> &term; | <emphasis role="bold">proof</emphasis>] [<emphasis role="bold">done</emphasis>]</para>
+ <para>[<emphasis role="bold">obtain</emphasis> &id; | <emphasis role="bold">conclude</emphasis> &term;] <emphasis role="bold">=</emphasis> &term; [&autoparams; | <emphasis role="bold">using</emphasis> &term; | <emphasis role="bold">using once</emphasis> &term; | <emphasis role="bold">proof</emphasis>] [<emphasis role="bold">done</emphasis>]</para>
</listitem>
</varlistentry>
<varlistentry>
<term>Pre-condition:</term>
<listitem>
- <para> &TODO; </para>
- </listitem>
+ <para><command>conclude</command> can be used only if the current
+ sequent is stating an equality. The left hand side must be omitted
+ in an equality chain.</para>
+ </listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
- <para> &TODO; </para>
+ <para>Starts or continues an equality chain. If the chain starts
+ with <command>obtain H</command> a new subproof named
+ <command>H</command> is started.</para>
</listitem>
</varlistentry>
<varlistentry>
- <term>New sequence to prove:</term>
+ <term>New sequent to prove:</term>
<listitem>
- <para> &TODO; </para>
+ <para>If the chain starts
+ with <command>obtain H</command> a nre sequent for
+ <command>t2 = ?</command> is opened.
+ </para>
</listitem>
</varlistentry>
</variablelist>
</para>
</sect1>
- <sect1 id="tac_bytermweproved">
- <title>by term we proved</title>
- <titleabbrev>by term we proved</titleabbrev>
- <para><userinput>by th we proved t [""|(id)]</userinput></para>
+ <sect1 id="tac_suppose">
+ <title>suppose</title>
+ <titleabbrev>suppose</titleabbrev>
+ <para><userinput>suppose t1 (x) that is equivalent to t2</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">suppose</emphasis> &term; <emphasis role="bold"> (</emphasis> &id;
+ <emphasis role="bold">) </emphasis> [ <emphasis role="bold">that is equivalent to</emphasis> &term; ]</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-condition:</term>
+ <listitem>
+ <para>The conclusion of the current proof must be
+ <command>∀x:T.P</command> or
+ <command>T→P</command> where <command>T</command> is
+ a proposition (i.e. <command>T</command> has type
+ <command>Prop</command> or <command>CProp</command>).</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It adds to the context of the current sequent to prove a new
+ declaration <command>x : T </command>. The new conclusion becomes
+ <command>P</command>.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+
+ <sect1 id="tac_thesisbecomes">
+ <title>the thesis becomes</title>
+ <titleabbrev>the thesis becomes</titleabbrev>
+ <para><userinput>the thesis becomes t</userinput></para>
<para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">by</emphasis> &term; <emphasis role="bold">we proved</emphasis> &term;
- <emphasis role="bold">(</emphasis> &id; <emphasis role="bold">)</emphasis></para>
- </listitem>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role ="bold">the thesis becomes</emphasis> &term; </para>
+ </listitem>
</varlistentry>
<varlistentry>
<term>Pre-condition:</term>
<listitem>
- <para><command>th</command>must have type <command>Prop</command>.
- <command>id</command>can to be omitted with null</para>
+ <para>The provided term <command>t</command> must be convertible with
+ current sequent.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
- <para>It closes the current sequent by applying<command>th</command> to <command>t</command>.</para>
+ <para>It changes the current goal to the one provided.</para>
</listitem>
</varlistentry>
<varlistentry>
- <term>New sequence to prove:</term>
+ <term>New sequent to prove:</term>
<listitem>
- <para> &TODO; </para>
+ <para>None.</para>
</listitem>
</varlistentry>
</variablelist>
</para>
- </sect1>
-
- <sect1 id="tac_exitselim">
- <title>exits elim</title>
- <titleabbrev>exits elim</titleabbrev>
- <para><userinput>by t let id:t such that t (id)</userinput></para>
+ </sect1>
+
+ <sect1 id="tac_weneedtoprove">
+ <title>we need to prove</title>
+ <titleabbrev>we need to prove</titleabbrev>
+ <para><userinput>we need to prove t1 (id) or equivalently t2</userinput></para>
<para>
<variablelist>
<varlistentry role="tactic.synopsis">
<term>Synopsis:</term>
<listitem>
- <para><emphasis role="bold">by</emphasis> &term; <emphasis role="bold">let</emphasis> &id;
- <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">such that</emphasis> &term;
- <emphasis role="bold">(</emphasis> &id; <emphasis role="bold">)</emphasis></para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-condition:</term>
- <listitem>
- <para><command>t</command> must be an inductive type,existential and
- <command>t (id)</command> must be an elimanation priciple for that inductive type.
- </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para>it proceeds on <command>t</command> to the elimination of the existential one </para>
+ <para><emphasis role="bold">we need to prove</emphasis> &term;
+ [<emphasis role="bold">(</emphasis>&id;
+ <emphasis role="bold">)</emphasis>]
+ [ <emphasis role="bold">or equivalently</emphasis> &term;]</para>
</listitem>
</varlistentry>
- <varlistentry>
- <term>New sequence to prove:</term>
+ <varlistentry>
+ <term>Pre-condition:</term>
<listitem>
- <para>It opens one new sequent. The names of the new hypotheses are picked by<command>t (id)</command> </para>
+ <para></para>
</listitem>
- </varlistentry>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>If <command>id</command> is provided, starts a subproof that once concluded
+ will be named <command>id</command>. Otherwise states what needs to be proved.
+ If <command>t2</command> is provided, the new goal is
+ immediately changed to <command>t2</command> wich must
+ be equivalent to <command>t1</command>.
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>The stated one if <command>id</command> is provided</para>
+ </listitem>
+ </varlistentry>
</variablelist>
</para>
</sect1>
+
<sect1 id="tac_andelim">
- <title>and elim</title>
- <titleabbrev>and elim</titleabbrev>
- <para><userinput>by t we have t (id) and t (id)</userinput></para>
+ <title>we have</title>
+ <titleabbrev>we have</titleabbrev>
+ <para><userinput>justification we have t1 (id1) and t2 (id2)</userinput>
+ </para>
<para>
<variablelist>
<varlistentry role="tactic_synopsis">
<term>Synopsis:</term>
<listitem>
- <para><emphasis role="bold">by</emphasis> &term; <emphasis role="bold">we have</emphasis> &term;
+ <para>&justification; <emphasis role="bold">we have</emphasis> &term;
<emphasis role="bold">( </emphasis> &id; <emphasis role="bold"> ) and </emphasis> &term;
<emphasis role="bold"> ( </emphasis> &id; <emphasis role="bold">)</emphasis></para>
</listitem>
<varlistentry>
<term>Pre-condition:</term>
<listitem>
- <para><command>t</command> must be an logical type,type and </para>
+ <para></para>
</listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
- <para>It proceeds on the values of <command>t</command>, according to the elimination principle </para>
+ <para>It derives <command>t1∧t2</command> using the
+ <command>justification</command> then it introduces in the context
+ <command>t1</command> labelled with <command>id1</command> and
+ <command>t2</command> labelled with <command>id2</command>.
+ </para>
</listitem>
</varlistentry>
<varlistentry>
- <term>New sequence to prove:</term>
+ <term>New sequent to prove:</term>
<listitem>
- <para>It opens one new sequent, the names of the new hypotheses are picked by <command>t(id) and t(id)</command> </para>
+ <para>None.</para>
</listitem>
</varlistentry>
</variablelist>
</para>
</sect1>
+ <sect1 id="tac_weproceedbycases">
+ <title>we proceed by cases on</title>
+ <titleabbrev>we proceed by cases on</titleabbrev>
+ <para><userinput>we proceed by cases on t to prove th</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">we proceed by cases on</emphasis> &term; <emphasis role="bold">to prove</emphasis> &term; </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-condition:</term>
+ <listitem>
+ <para><command>t</command> must inhabitant of an inductive type and
+ <command>th</command> must be the conclusion to be proved by
+ cases.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para> It proceeds by cases on <command>t</command> </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>It opens one new sequent for each constructor of the
+ type of <command>t</command>.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+
+ <sect1 id="tac_weproceedbyinduction">
+ <title>we proceed by induction on</title>
+ <titleabbrev>we proceed by induction on</titleabbrev>
+ <para><userinput>we proceed by induction on t to prove th</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">we proceed by induction on</emphasis> &term; <emphasis role="bold"> to prove </emphasis> &term; </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-condition:</term>
+ <listitem>
+ <para><command>t</command> must inhabitant of an inductive type and
+ <command>th</command> must be the conclusion to be proved by induction.
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It proceed by induction on <command>t</command>.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>It opens one new sequent for each constructor of the
+ type of <command>t</command>.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+
+
+ <sect1 id="tac_bytermweproved">
+ <title>we proved</title>
+ <titleabbrev>we proved</titleabbrev>
+ <para><userinput>justification we proved t (id)</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para>&justification; <emphasis role="bold">we proved</emphasis> &term;
+ <emphasis role="bold">(</emphasis> &id;
+ <emphasis role="bold">)</emphasis></para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-condition:</term>
+ <listitem>
+ <para><command>t</command>must have type <command>Prop</command>.
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It derives <command>t</command>
+ using the justification and labels the conclusion with
+ <command>id</command>.
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequent to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+
</chapter>
projects / helm.git / blobdiff