permute some paragraphs

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@14135 3260e6d1-4efc-4170-b0a7-36055960796d

C11-FrontEnd/C_Appendices.thy

@@ -355,6 +355,24 @@ showing the content of the virtual file-system in the left window. Selecting and
 in the latter lets jEdit display it in a new buffer, which gives the possibility to export this file
 via \<open>File\<rightarrow>Save As\<close> into the real file-system.\<close>
 
+section\<open>Exporting C Files to the File-System\<close>
+
+text\<open>From the Isabelle/C side, the task is easy, just type:\<close>
+
+C_export_file
+
+text\<open>... which does the trick and generates a file \<^verbatim>\<open>C1.c\<close>. But hold
+on --- where is it?  Well, Isabelle/C uses since version Isabelle2019 a virtual
+file-system. Exporting from it to the real file-system requires a few mouse-clicks (unfortunately).
+
+So activating the command \<^theory_text>\<open>C_export_file\<close> leads to the output
+\<^verbatim>\<open>See theory exports "C/*/C1.c"\<close> (see figure
+\<^verbatim>\<open>C-export-example.png\<close>), and clicking on the highlighted
+\<^verbatim>\<open>theory exports\<close> lets Isabelle display a part of the virtual file-system
+(see subwidget left). Activating it in the subwidget lets jEdit open it as an editable file, which
+can be exported via \<^verbatim>\<open>File->Save As->...\<close> into the real file-system.
+\<close>
+
 section \<open>Case Study: Mapping on the Parsed AST\<close>
 
 text \<open> In this section, we give a concrete example of a situation where one is interested to

C11-FrontEnd/examples/C1.thy

@@ -861,22 +861,4 @@ int main () {
 }
 \<close>
 
-section\<open>Exporting C Files to the File-System\<close>
-
-text\<open>From the Isabelle/C side, the task is easy, just type:\<close>
-
-C_export_file
-
-text\<open>... which does the trick and generates a file \<^verbatim>\<open>C1.c\<close>. But hold
-on --- where is it?  Well, Isabelle/C uses since version Isabelle2019 a virtual
-file-system. Exporting from it to the real file-system requires a few mouse-clicks (unfortunately).
-
-So activating the command \<^theory_text>\<open>C_export_file\<close> leads to the output
-\<^verbatim>\<open>See theory exports "C/*/C1.c"\<close> (see figure
-\<^verbatim>\<open>C-export-example.png\<close>), and clicking on the highlighted
-\<^verbatim>\<open>theory exports\<close> lets Isabelle display a part of the virtual file-system
-(see subwidget left). Activating it in the subwidget lets jEdit open it as an editable file, which
-can be exported via \<^verbatim>\<open>File->Save As->...\<close> into the real file-system.
-\<close>
-
 end