syntactic rearrangements

examples/CENELEC_50128/mini_odo/mini_odo.thy

@@ -294,7 +294,7 @@ and the global model parameters such as wheel diameter, the number of teeth per
 sampling frequency etc., we can infer the maximal time of service as well the maximum distance 
 the device can measure.  As an example configuration, choosing:
 
-   \<^item> \<^term>\<open>(1 *\<^sub>Q metre)::real[m]\<close>      for  \<^term>\<open>w\<^sub>d\<close>   (wheel-diameter), 
+   \<^item> \<^term>\<open>(1 *\<^sub>Q metre):: real[m]\<close>      for  \<^term>\<open>w\<^sub>d\<close>   (wheel-diameter), 
    \<^item> \<^term>\<open>100         :: real\<close>        for  \<^term>\<open>tpw\<close> (teeth per wheel), 
    \<^item> \<^term>\<open>80 *\<^sub>Q kmh   :: real[m\<cdot>s\<^sup>-\<^sup>1]\<close>  for  \<^term>\<open>Speed\<^sub>M\<^sub>a\<^sub>x\<close>,
    \<^item> \<^term>\<open>14.4 *\<^sub>Q kHz :: real[s\<^sup>-\<^sup>1]\<close>    for the sampling frequency,
@@ -654,9 +654,9 @@ text*[t10::test_result]
   test-execution via, \<^eg>, a makefile or specific calls to a test-environment or test-engine. \<close>
 
 
-text
-\<open>  Finally some examples of references to doc-items, i.e. text-elements 
-   with declared  meta-information and status. \<close> 
+text \<open> Finally some examples of references to doc-items, i.e. text-elements 
+       with declared  meta-information and status. \<close> 
+
 text \<open> As established by @{test_result (unchecked) \<open>t10\<close>}, 
                          @{test_result (define) \<open>t10\<close>} \<close>
 text \<open> the               @{test_result \<open>t10\<close>}                      

src/DOF/Isa_COL.thy

@@ -353,7 +353,7 @@ text\<open>Tables are (sub) document-elements represented inside the documentati
 language. The used technology is similar to the existing railroad-diagram support 
 (cf. \<^url>\<open>https://isabelle.in.tum.de/doc/isar-ref.pdf\<close>, Sec. 4.5). 
 
-However, tables are not directly based on the ideosynchrasies of Knuth-based language design ---
+However, tables are not directly based on the idiosyncrasies of Knuth-based language design ---
 
 However, tables come with a more abstract structure model than conventional typesetting in the 
 LaTeX tradition. It is based of the following principles:

src/tests/Isabelle2021-1.thy

@@ -196,6 +196,8 @@ text \<open>
   example:
 
     \<^ML>\<open>\<^Type>\<open>nat\<close>\<close>
+    \<^ML>\<open>\<^Type>\<open>prod \<^Type>\<open>int\<close> \<^Type>\<open>int\<close>\<close>\<close>
+
     \<^ML>\<open>fn (A, B) => \<^Type>\<open>fun A B\<close>\<close>
     \<^ML>\<open>\<^Type_fn>\<open>fun A B => \<open>(A, B)\<close>\<close>\<close>
 

src/tests/OutOfOrderPresntn.thy

@@ -352,8 +352,8 @@ Config.get ;
 
 (*
 \begin{figure}[h]
-
      \centering
+
      \includegraphics[scale=0.5]{graph_a}
      \caption{An example graph}
 
@@ -362,35 +362,37 @@ Config.get ;
 
 
 \begin{figure}
-
      \centering
+
      \begin{subfigure}[b]{0.3\textwidth}
 
          \centering
          \includegraphics[width=\textwidth]{graph1}
          \caption{$y=x$}
 
-         \label{fig:y equals x}
+         \label{fig:y equals x}   (* PROBLEM *)
      \end{subfigure}
 
      \hfill
+
      \begin{subfigure}[b]{0.3\textwidth}
 
          \centering
          \includegraphics[width=\textwidth]{graph2}
          \caption{$y=3sinx$}
 
-         \label{fig:three sin x}
+         \label{fig:three sin x}  (* PROBLEM *)
      \end{subfigure}
 
      \hfill
+
      \begin{subfigure}[b]{0.3\textwidth}
 
          \centering
          \includegraphics[width=\textwidth]{graph3}
          \caption{$y=5/x$}
 
-         \label{fig:five over x}
+         \label{fig:five over x} (* PROBLEM *)
      \end{subfigure}
 
   \caption{Three simple graphs}