Use amsthm.sty to define 'definition' environment

This may, we get a referencing mechanism that also works with LaTeXML.

chapters/classes.tex

@@ -961,10 +961,8 @@ \section{Balanced Models}\doublelabel{balanced-models}
 components are included -- possibly modified. The corresponding
 restrictions on connectors and connections are in \autoref{restrictions-of-connections-and-connectors}.
 
-\numbereddefinition{Local Number of Unknowns}
-
-The \firstuse{local number of unknowns} of a model or block class is the sum based
-on the components:
+\begin{definition}[Local number of unknowns]
+The local number of unknowns of a model or block class is the sum based on the components:
 \begin{itemize}
 \item
   For each declared component of specialized class \lstinline!type! (Real, Integer,
@@ -991,11 +989,10 @@ \section{Balanced Models}\doublelabel{balanced-models}
   the elements after expanding all records and arrays to a set of
   scalars of primitive types).
 \end{itemize}
+\end{definition}
 
-\numbereddefinition{Local Equation Size}
-
-The \firstuse{local equation size} of a model or block class is the sum of the
-following numbers:
+\begin{definition}[Local equation size]
+The local equation size of a model or block class is the sum of the following numbers:
 \begin{itemize}
 \item
   The number of equations defined locally (i.e.\ not in any model or
@@ -1016,6 +1013,7 @@ \section{Balanced Models}\doublelabel{balanced-models}
   I.e., top-level inputs are treated as known variables.  This represents the number of binding equations that will be provided when the class is used.
   \end{nonnormative}
 \end{itemize}
+\end{definition}
 
 \begin{nonnormative}
 To clarify top-level inputs without binding equation (for
@@ -1035,20 +1033,17 @@ \section{Balanced Models}\doublelabel{balanced-models}
 supplied when using the model.
 \end{nonnormative}
 
-\numbereddefinition{Locally Balanced}
-
-A model or block class is \firstuse{locally balanced} if the
-\emph{local number of unknowns} is identical to the \emph{local equation size} for all legal
-values of constants and parameters.
+\begin{definition}[Locally balanced]
+A model or block class is locally balanced if the \emph{local number of unknowns} is identical to the \emph{local equation size} for all legal values of constants and parameters.
+\end{definition}
 
 \begin{nonnormative}
 Here, \emph{legal values} must respect final bindings and min/max-restrictions.  A tool shall verify the \emph{locally balanced} property for the actual
 values of parameters and constants in the simulation model.  It is a quality of implementation for a tool to verify this property in general, due to
 arrays of (locally) undefined sizes, conditional declarations, for loops etc.
 \end{nonnormative}
 
-\numbereddefinition{Globally Balanced}
-
+\begin{definition}[Globally balanced]
 Similarly as locally balanced, but including all unknowns and equations
 from all components. The global number of unknowns is computed by
 expanding all unknowns (i.e.\ excluding parameters and constants) into a
@@ -1067,6 +1062,7 @@ \section{Balanced Models}\doublelabel{balanced-models}
   I.e., top-level inputs are treated as known variables.
   \end{nonnormative}
 \end{itemize}
+\end{definition}
 
 The following restrictions hold:
 \begin{itemize}

chapters/interface.tex

@@ -457,8 +457,7 @@ \section{Plug-Compatibility or Restricted Subtyping}\doublelabel{plug-compatibil
 connected by default.
 \end{nonnormative}
 
-\numbereddefinition{Plug-compatibility (= restricted subtyping)}
-
+\begin{definition}[Plug-compatibility (= restricted subtyping)]
 An interface \lstinline!A! is plug-compatible with (a restricted subtype of) an
 interface \lstinline!B! (or the constraining interface of \lstinline!B!) iff:
 \begin{itemize}
@@ -468,9 +467,9 @@ \section{Plug-Compatibility or Restricted Subtyping}\doublelabel{plug-compatibil
   All public components present in \lstinline!A! but not in \lstinline!B! must be
   default-connectable (as defined below).
 \end{itemize}
+\end{definition}
 
-\numbereddefinition{Default connectable}
-
+\begin{definition}[Default connectable]
 A component of an interface is default-connectable iff:
 \begin{itemize}
 \item
@@ -490,6 +489,7 @@ \section{Plug-Compatibility or Restricted Subtyping}\doublelabel{plug-compatibil
   binding equation or all of its sub-components must have binding
   equations.
 \end{itemize}
+\end{definition}
 
 Based on the above definitions, there are the following restrictions:
 \begin{itemize}
@@ -572,8 +572,7 @@ \section{Function-Compatibility or Function-Subtyping for Functions}\doublelabel
 existing calls.
 \end{nonnormative}
 
-\numbereddefinition{Function-Compatibility or Function-Subtyping for Functions}
-
+\begin{definition}[Function-compatibility or function-subtyping for functions]
 A function class \lstinline!A! is \emph{function-compatible with or a function
 subtype of} function class \lstinline!B! iff (the terms \emph{function-compatible}
 and \emph{function subtype} of are synonyms and used interchangeably):
@@ -595,6 +594,7 @@ \section{Function-Compatibility or Function-Subtyping for Functions}\doublelabel
   A public input component of \lstinline!A! not present in \lstinline!B! must have a binding
   assignment.
 \end{itemize}
+\end{definition}
 
 Based on the above definition the following restriction holds:
 \begin{itemize}

preamble.tex

@@ -140,11 +140,30 @@
 % henrikt-ma: Introducing semantic macro for 7 definitions spread out over two chapters
 % that for unclear reasons use their own style, including numbering.  Sorting out if numbered
 % definitions should be used more or not at all is part of issue #2570.
-\newcounter{defnumber}
-\newcommand{\numbereddefinition}[1]{%
-\stepcounter{defnumber}%
-\paragraph*{Definition~\thedefnumber: #1.}%
-}
+%
+% Definitions are numbered, but are not suitable for use with \autoref, as \autoref is not aware
+% of our custom definitions.  (They say there are better alternatives to \autoref, more suited
+% for this kind of customization...)  To avoid accidental use of \autoref, a definition should
+% also avoid use of \doublelabel, and instead use \definitionlabel.  Instead of \autoref, the definition
+% should be referenced using \definitionref
+%
+% If we'd like to have definitions spanning over several paragraphs, we should use an environment
+% instead of a command, but then we also need to find a way to visualize where the definition ends;
+% alternatives that come to mind include boxes, indentation, a right-flushed black square, but the
+% big challenge would be to find something that also works well with LaTeXML.
+\usepackage{amsthm}
+\newtheoremstyle{mlsdefinition}
+  {\topsep}   % ABOVESPACE
+  {\topsep}   % BELOWSPACE
+  {}          % BODYFONT
+  {}          % INDENT (empty value is the same as 0pt)
+  {\bfseries} % HEADFONT
+  {.}         % HEADPUNCT
+  {.75em}     % HEADSPACE
+  {Definition~#2. \firstuse{#3}}        % CUSTOM-HEAD-SPEC
+\theoremstyle{mlsdefinition}
+\newtheorem{definition}{Definition}[chapter]
+\newcommand{\definitionautorefname}{definition}
 
 \setcounter{secnumdepth}{5}
 % Note: Toc changed for appendex