update links

C11-FrontEnd/appendices/C_Appendices.thy

@@ -315,19 +315,19 @@ text \<open>
 section \<open>Quick Start (for People More Familiar with C than Isabelle)\<close>
 
 text \<open>
-\<^item> Assuming we are working with Isabelle 2019
-\<^url>\<open>http://isabelle.in.tum.de/dist/Isabelle2019_app.tar.gz\<close>, the shortest way to
+\<^item> Assuming we are working with Isabelle 2021
+\<^url>\<open>https://isabelle.in.tum.de/website-Isabelle2021/dist/Isabelle2021_linux.tar.gz\<close>, the shortest way to
 start programming in C is to open a new theory file with the shell-command:
 
 \<^verbatim>\<open>$ISABELLE_HOME/bin/isabelle jedit -d $AFP_HOME/thys Scratch.thy\<close>
 
 where \<^verbatim>\<open>$ISABELLE_HOME\<close> is the path of the above extracted Isabelle source,
 and \<^verbatim>\<open>$AFP_HOME\<close> is the downloaded content of
-\<^url>\<open>https://bitbucket.org/isa-afp/afp-2019\<close>.\<^footnote>\<open>This folder
+\<^url>\<open>https://foss.heptapod.net/isa-afp/afp-2021\<close>.\<^footnote>\<open>This folder
 particularly contains the Isabelle/C project, located in
-\<^url>\<open>https://bitbucket.org/isa-afp/afp-2019/src/default/thys/Isabelle_C\<close>. To inspect
+\<^url>\<open>https://foss.heptapod.net/isa-afp/afp-2021/-/tree/branch/default/thys/Isabelle_C\<close>. To inspect
 the latest developper version, one can also replace \<^verbatim>\<open>$AFP_HOME/thys\<close> by the
-content downloaded from \<^url>\<open>https://gitlri.lri.fr/ftuong/isabelle_c\<close>.\<close>
+content downloaded from \<^url>\<open>https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C\<close>.\<close>
 \<^item> The next step is to copy this minimal content inside the newly opened window:
 \<^verbatim>\<open>theory Scratch imports Isabelle_C.C_Main begin C \<open>
 // C code
@@ -532,7 +532,7 @@ text \<open> Generally, semantic back-ends can be written in full ML starting fr
 \<^ML_type>\<open>C_Ast.CTranslUnit\<close>, but to additionally support formalizing tasks requiring
 to start from an AST defined in Isabelle/HOL, we provide an equivalent AST in HOL in the project,
 such as the one obtained after loading
-\<^url>\<open>https://gitlri.lri.fr/ftuong/citadelle-devel/blob/master/doc/Meta_C_generated.thy\<close>.
+\<^url>\<open>https://gitlab.lisn.upsaclay.fr/frederictuong/isabelle_contrib/-/blob/master/Citadelle/doc/Meta_C_generated.thy\<close>.
 (In fact, the ML AST is just generated from the HOL one.) \<close>
 
 
@@ -618,7 +618,7 @@ interest.
 \<close>
 
 section \<open>Known Limitations, Troubleshooting\<close>
-subsection \<open>The Document Model of the Isabelle/PIDE (applying for Isabelle 2019)\<close>
+subsection \<open>The Document Model of the Isabelle/PIDE (applying since at least Isabelle 2019)\<close>
 subsubsection \<open>Introduction\<close>
 
 text \<open> Embedding C directives in C code is an act of common practice in numerous applications,

C11-FrontEnd/src/C_Ast.thy

@@ -85,7 +85,7 @@ text \<open> For the case of \<^file>\<open>../generated/c_ast.ML\<close>, it is
 mandatory to have a ``physical'' representation of the file in \<^dir>\<open>../generated\<close>:
 it could be generated ``on-the-fly'' with \<^theory_text>\<open>code_reflect\<close> and immediately
 loaded: Citadelle has an option to choose between the two
-tasks~\cite{DBLP:journals/afp/TuongW15}.\<^footnote>\<open>\<^url>\<open>https://gitlri.lri.fr/ftuong/citadelle-devel\<close>\<close>\<close>
+tasks~\cite{DBLP:journals/afp/TuongW15}.\<^footnote>\<open>\<^url>\<open>https://gitlab.lisn.upsaclay.fr/frederictuong/isabelle_contrib/-/tree/master/Citadelle/src/compiler\<close>\<close>\<close>
 
 text \<open> After loading the AST, it is possible in Citadelle to do various meta-programming
 renaming, such as the one depicted in the next command. Actually, its content is explicitly included