From 03d2931aad83cb7ce7383ee87fa80c108ac33dac Mon Sep 17 00:00:00 2001
From: Tanaka Akira
Date: Fri, 25 Jan 2019 01:55:05 +0900
Subject: Move \def\plus and \def\tri to refman-preamble.sty.

The definition of \plus and \tri in cic.rst is not effective
for HTML output.

So, move them into refman-preamble.sty.

Also, \tri is renamed to \trii to express
the suffix of "\triangleright_\iota".
---
 doc/sphinx/language/cic.rst | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)

(limited to 'doc/sphinx/language')

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 91504089a8..25a230015c 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1719,13 +1719,11 @@ possible:
 .. math::
    :nowrap:
 
-   {\def\plus{\mathsf{plus}}
-    \def\tri{\triangleright_\iota}
-    \begin{eqnarray*}
-    \plus~(\nS~(\nS~\nO))~(\nS~\nO) & \tri & \nS~(\plus~(\nS~\nO)~(\nS~\nO))\\
-                                   & \tri & \nS~(\nS~(\plus~\nO~(\nS~\nO)))\\
-                                   & \tri & \nS~(\nS~(\nS~\nO))\\
-    \end{eqnarray*}}
+   \begin{eqnarray*}
+   \plus~(\nS~(\nS~\nO))~(\nS~\nO)~& \trii & \nS~(\plus~(\nS~\nO)~(\nS~\nO))\\
+                                   & \trii & \nS~(\nS~(\plus~\nO~(\nS~\nO)))\\
+                                   & \trii & \nS~(\nS~(\nS~\nO))\\
+   \end{eqnarray*}
 
 .. _Mutual-induction:
 
-- 
cgit v1.2.3