- <listitem>It is based on a variant of the Calculus of (co)Inductive
- Constructions (CIC). CIC is also the logic of the Coq proof assistant.
- </listitem>
- <listitem>It adopts a procedural proof language, but it has a new
- set of small step tacticals that improve proof structuring and debugging.
- </listitem>
- <listitem>It has a stand-alone graphical user interface (GUI) inspired by
- CtCoq/Proof General. The GUI is implemented according to the state
- of the art. In particular:
- <itemizedlist>
- <listitem>It is based and fully integrated with Gtk/Gnome.</listitem>
- <listitem>An on-line help can be browsed via the Gnome documentation
- browser.</listitem>
- <listitem>Mathematical formulae are rendered in two dimensional
- notation via MathML and Unicode.</listitem>
- </itemizedlist>
- </listitem>
- <listitem>It integrates advanced browsing and searching procedures.
- </listitem>
- <listitem>It allows the use of the typical ambiguous mathematical notation
- by means of a disambiguating parser.
- </listitem>
- <listitem>It is compatible with the library of Coq (definitions and
- proof objects).
- </listitem>
+ <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>
+ </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>
+ </listitem>
+ <listitem>
+ <para>It has a stand-alone graphical user interface (GUI) inspired by
+CtCoq/Proof General. The GUI is implemented according to the state
+of the art. In particular:</para>
+ <itemizedlist>
+ <listitem>
+ <para>It is based and fully integrated with Gtk/Gnome.</para>
+ </listitem>
+ <listitem>
+ <para>An on-line help can be browsed via the Gnome documentation browser.</para>
+ </listitem>
+ <listitem>
+ <para>Mathematical formulae are rendered in two dimensional notation via MathML and Unicode.</para>
+ </listitem>
+ </itemizedlist>
+ </listitem>
+ <listitem>
+ <para>It integrates advanced browsing and searching procedures.</para>
+ </listitem>
+ <listitem>
+ <para>It allows the use of the typical ambiguous mathematical notation by means of a disambiguating parser.</para>
+ </listitem>
+ <listitem>
+ <para>It is compatible with the library of Coq (definitions and proof objects).</para>
+ </listitem>