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

C11-FrontEnd/C_Main.thy

@@ -94,14 +94,9 @@ val _ =
 end
 \<close>
 
-section\<open>Definition of the Command "C_file"\<close>
+section\<open>The Command "C_file"\<close>
 
 ML\<open>
-(*  Title:      Pure/ML/ml_file.ML
-    Author:     Makarius
-
-Commands to load ML files.
-*)
 
 structure C_File =
 struct
@@ -124,7 +119,7 @@ val C : (theory -> Token.file list) ->
 end;
 \<close>
 
-section \<open>Pure\<close>
+section \<open>Reading and Writing C-Files\<close>
 
 ML\<open>
 local
@@ -143,7 +138,7 @@ val _ =
 in end
 \<close>
 
-section \<open>\<close>
+section \<open>ML-Antiquotations for Debugging\<close>
 
 ML\<open>
 fun print_top make_string f _ (_, (value, pos1, pos2)) _ thy =

C11-FrontEnd/examples/C1.thy

@@ -471,8 +471,8 @@ section \<open>Miscellaneous\<close>
 C \<comment> \<open>Antiquotations acting on a parsed-subtree\<close> \<open>
 # /**/ include  <a\b\\c> // backslash rendered unescaped
 f(){0 +  0;} /**/  // val _ : theory => 'a => theory
-# /*@ context */ if if elif
-#include
+# /* context */ if if elif
+#include <stdio.h>
 if then else ;
 # /* zzz */  elif /**/
 #else\