[refman] support of logic functions and predicates

src/plugins/e-acsl/doc/refman/changes_modern.tex

@@ -124,6 +124,11 @@ in \lstinline|\\at|}
     {
 \section{Changes in \eacsl Implementation}
 
+\subsection*{Version \eacslversion}
+\begin{itemize}
+\item \changeinsection{logicspec}{support of logic functions and predicates}
+\end{itemize}
+
 \subsection*{Version Argon-18}
 
 \begin{itemize}

src/plugins/e-acsl/doc/refman/logic.tex

 \begin{syntax}
-  C-global-decl ::= { "/*@" logic-def+ "*/" }
+  C-global-decl ::= "/*@" logic-def+ "*/"
   \
-  [ { logic-def } ] ::= { logic-const-def } ;
-          | { logic-function-def } ;
-          | { logic-predicate-def } ;
+  logic-def ::= { logic-const-def } ;
+          | logic-function-def ;
+          | logic-predicate-def ;
   \
-  [ { type-expr } ] ::= { id };
+  type-expr ::= id;
   \
-  [ { logic-const-def } ] ::= { "logic" type-expr id "=" term ";" }
+  { logic-const-def } ::= { "logic" type-expr id "=" term ";" }
   \
-  [ { logic-function-def } ] ::= { "logic" type-expr id parameters "=" term ";" }
+  logic-function-def ::= "logic" type-expr id parameters "=" term ";"
   \
-  [ { logic-predicate-def } ] ::= { "predicate" id parameters? "=" pred ";" }
+  logic-predicate-def ::= "predicate" id parameters? "=" pred ";"
   \
-  { parameters } ::= { "(" parameter (, parameter)* ")" }
+  parameters ::= "(" parameter (, parameter)* ")"
   \
-  { parameter } ::= { type-expr id }
+  parameter ::= type-expr id
 \end{syntax}

src/plugins/e-acsl/doc/refman/speclang_modern.tex

@@ -612,7 +612,7 @@ axiomatics.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\subsection{\notimplemented{Predicate and function definitions}}
+\subsection{Predicate and function definitions}
 \nodiff
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -642,7 +642,7 @@ axiomatics.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\subsection{\notimplemented{Recursive logic definitions}}
+\subsection{Recursive logic definitions}
 \index{recursion}
 \nodiff