diff --git a/C11-FrontEnd/C_Appendices.thy b/C11-FrontEnd/C_Appendices.thy
index 91ec840b0d6fba3ccd9dd5c66dbb968122f3dfc3..d45afb7391cac7063d4a780bcc14c6ec4a62b886 100644
--- a/C11-FrontEnd/C_Appendices.thy
+++ b/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
diff --git a/C11-FrontEnd/examples/C_paper.thy b/C11-FrontEnd/examples/C_paper.thy
index d365e7da32c2571b61da6e69a3c8fdbb79d8e9ef..4b8948be929c38e8e8f552dbfd5c36a0457e2aa1 100644
--- a/C11-FrontEnd/examples/C_paper.thy
+++ b/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