synchronize with gitlab.lri.fr:ftuong/isabelle_c 76c05ee4

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

C11-FrontEnd/C_Appendices.thy

@@ -787,7 +787,7 @@ make the error disappear at the position the error is indicated can be detailed
   \<^file>\<open>../C11-BackEnds/AutoCorres_wrapper/examples/TestSEL4.thy\<close> is already provided as
   preprocessed). Another way would be adding a specific new semantic back-end implementing the
   automation of the preprocessing task (as done in
-  \<^file>\<open>../C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_TEC.thy\<close>, where the
+  \<^file>\<open>../C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_linear_CCT.thy\<close>, where the
   back-end explicitly makes a call to \<open>cpp\<close> at run-time).
 
   \<^item> Ultimately, modifying the grammar with new rules cancelling the exception would only work

C11-FrontEnd/examples/C_paper.thy

@@ -143,7 +143,7 @@ int a (int b) { return &a + b + c; }
 
 section \<open>Proofs inside C-Annotations\<close>
 
-\<comment> \<open>See also: \<^file>\<open>../../C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_TEC.thy\<close>\<close>
+\<comment> \<open>See also: \<^file>\<open>../../C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_linear_CCT.thy\<close>\<close>
 
 C \<open>
 #define SQRT_UINT_MAX 65536