From 6649b4c0c431c1ae4133629e324b6dd74feccd29 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Tuong?=
<tuong@users.noreply.github.com>
Date: Mon, 4 May 2020 20:04:54 +0000
Subject: [PATCH] synchronize with gitlab.lri.fr:ftuong/isabelle_c
76c05ee4337c8257a3a63f530530a394803208be
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 | 2 +-
C11-FrontEnd/examples/C_paper.thy | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/C11-FrontEnd/C_Appendices.thy b/C11-FrontEnd/C_Appendices.thy
index 91ec840b0d6..d45afb7391c 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 d365e7da32c..4b8948be929 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
--
GitLab