]> matita.cs.unibo.it Git - helm.git/commitdiff
consistent naming of the calculus
authorStefano Zacchiroli <zack@upsilon.cc>
Sat, 10 Jun 2006 16:21:25 +0000 (16:21 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Sat, 10 Jun 2006 16:21:25 +0000 (16:21 +0000)
matita/help/C/sec_gettingstarted.xml
matita/help/C/sec_intro.xml

index 27e373295ac8f16fee09fba572e9329ebed8a716..b067e21ec409f004deffeafc2b4aa001a4a63778 100644 (file)
@@ -3,7 +3,7 @@
 
 <chapter id="sec_gettingstarted">
   <title>Getting started</title>
-  <para> If you are already familiar with the Calculus of (co)Inductive
+  <para> If you are already familiar with the Calculus of (Co)Inductive
   Constructions (CIC) and with interactive theorem provers with procedural
   proof languages (expecially Coq), getting started with Matita is relatively
   easy. You just need to learn how to type Unicode symbols, how to browse
index 773bda24ca7f86fe0e0cba580a3e5f6e103d6b98..6c22f46647fe4dad91567fefc8f3af95c5b82634 100644 (file)
@@ -9,7 +9,7 @@
       (or proof assistant) with the following characteristics:</para>
     <itemizedlist>
       <listitem>
-        <para>It is based on a variant of the Calculus of (co)Inductive Constructions (CIC). CIC is also the logic of the Coq proof assistant.</para>
+        <para>It is based on a variant of the Calculus of (Co)Inductive Constructions (CIC). CIC is also the logic of the Coq proof assistant.</para>
       </listitem>
       <listitem>
         <para>It adopts a procedural proof language, but it has a new set of small step tacticals that improve proof structuring and debugging.</para>