CLEANUP: superfluous examples were removed

2 files changed, 6 insertions, 16 deletions

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 0ea2ed650..a6240ad28 100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -281,7 +281,7 @@
 \newcommand{\unfold}{\mbox{\textsf{unfold}}}
 \newcommand{\zeros}{\mbox{\textsf{zeros}}}
 \newcommand{\even}{\mbox{\textsf{even}}}
-\newcommand{\odd}{\mbox{\textsf{even}}}
+\newcommand{\odd}{\mbox{\textsf{odd}}}
 \newcommand{\evenO}{\mbox{\textsf{even\_O}}}
 \newcommand{\evenS}{\mbox{\textsf{even\_S}}}
 \newcommand{\oddS}{\mbox{\textsf{odd\_S}}}
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 101c4e503..d3e8755a8 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -763,21 +763,11 @@ these two inference rules above enable us to conclude that:
 \vskip.5em
 \def\prefix{E[\Gamma]\vdash\hskip.25em}
 $\begin{array}{@{} l}
-   \prefix\bool : \Set\\
-   \prefix\true : \bool\\
-   \prefix\false : \bool\\
-   \prefix\nat : \Set\\
-   \prefix\nO : \nat\\
-   \prefix\nS : \nat\ra\nat\\
-   \prefix\List : \Type\ra\Type\\
-   \prefix\Nil : \forall~A\!:\!\Type,~\List~A\\
-   \prefix\cons : \forall~A\!:\!\Type,~A\ra\List~A\ra\List~A\\
-   \prefix\haslength : \forall~A\!:\!\Type,~\List~A\ra\nat\ra\Prop\\
-   \prefix\nilhl : \forall~A\!:\!\Type,~\haslength~A~(\Nil~A)~\nO\\
-   \begin{array}{l l}
-   \hskip-.5em\prefix\conshl :\hskip-.5em & \forall~A\!:\!\Type,~\forall~a\!:\!A,~\forall~l\!:\!\List~A,~\forall~n\!:\!\nat,\\
-                            & \haslength~A~l~n\ra \haslength~A~(\cons~A~a~l)~(\nS~n)
-   \end{array}
+   \prefix\even : \nat\ra\Prop\\
+   \prefix\odd : \nat\ra\Prop\\
+   \prefix\evenO : \even~\nO\\
+   \prefix\evenS : \forall~n:\nat, \odd~n \ra \even~(\nS~n)\\
+   \prefix\oddS : \forall~n:\nat, \even~n \ra \odd~(\nS~n)
  \end{array}$
 
 %\paragraph{Parameters.}