From cce6f6dc86e2891f87b2023f35ccc5d73a10a5dd Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Sat, 10 Jun 2006 16:21:25 +0000 Subject: [PATCH] consistent naming of the calculus --- helm/software/matita/help/C/sec_gettingstarted.xml | 2 +- helm/software/matita/help/C/sec_intro.xml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/matita/help/C/sec_gettingstarted.xml b/helm/software/matita/help/C/sec_gettingstarted.xml index 27e373295..b067e21ec 100644 --- a/helm/software/matita/help/C/sec_gettingstarted.xml +++ b/helm/software/matita/help/C/sec_gettingstarted.xml @@ -3,7 +3,7 @@ Getting started - If you are already familiar with the Calculus of (co)Inductive + 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 diff --git a/helm/software/matita/help/C/sec_intro.xml b/helm/software/matita/help/C/sec_intro.xml index 773bda24c..6c22f4664 100644 --- a/helm/software/matita/help/C/sec_intro.xml +++ b/helm/software/matita/help/C/sec_intro.xml @@ -9,7 +9,7 @@ (or proof assistant) with the following characteristics: - It is based on a variant of the Calculus of (co)Inductive Constructions (CIC). CIC is also the logic of the Coq proof assistant. + It is based on a variant of the Calculus of (Co)Inductive Constructions (CIC). CIC is also the logic of the Coq proof assistant. It adopts a procedural proof language, but it has a new set of small step tacticals that improve proof structuring and debugging. -- 2.39.2