diff --git a/C11-BackEnds/AutoCorres_wrapper/examples/BinarySearch.thy b/C11-BackEnds/AutoCorres_wrapper/examples/BinarySearch.thy
index fb6f254e95605f73f2fea7674c9c17a3883c4e7f..24a9902279babc87d9e9a17571402f3ad55a4edb 100644
--- a/C11-BackEnds/AutoCorres_wrapper/examples/BinarySearch.thy
+++ b/C11-BackEnds/AutoCorres_wrapper/examples/BinarySearch.thy
@@ -1,6 +1,7 @@
 (******************************************************************************
  * Isabelle/C/AutoCorres
  *
+ * Copyright (c) 2014, NICTA (for the C example)
  * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France
  *
  * All rights reserved.
diff --git a/C11-BackEnds/AutoCorres_wrapper/examples/CList.thy b/C11-BackEnds/AutoCorres_wrapper/examples/CList.thy
index 49ce4bb4470c958fb98d363b00f1ea1a6f6daa95..5f66fdd34eaf56facdccf9596a1abefab48015f3 100644
--- a/C11-BackEnds/AutoCorres_wrapper/examples/CList.thy
+++ b/C11-BackEnds/AutoCorres_wrapper/examples/CList.thy
@@ -1,6 +1,9 @@
 (******************************************************************************
  * Isabelle/C/AutoCorres
  *
+ * Copyright (C) 2002 Tobias Nipkow (TUM)
+ * Copyright (C) 2013--2014 Japheth Lim (NICTA)
+ * Copyright (C) 2013--2014 David Greenaway (NICTA)
  * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France
  *
  * All rights reserved.
diff --git a/C11-BackEnds/AutoCorres_wrapper/examples/FactorialTest.thy b/C11-BackEnds/AutoCorres_wrapper/examples/FactorialTest.thy
index 2ac208d654953c72246c1a63a8809fe1b6a549e0..a57e3c32f0b55807d72c274fa78838a57ca1bdb4 100644
--- a/C11-BackEnds/AutoCorres_wrapper/examples/FactorialTest.thy
+++ b/C11-BackEnds/AutoCorres_wrapper/examples/FactorialTest.thy
@@ -1,6 +1,7 @@
 (******************************************************************************
  * Isabelle/C/AutoCorres
  *
+ * Copyright 2014, NICTA
  * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France
  *
  * All rights reserved.
diff --git a/C11-BackEnds/AutoCorres_wrapper/examples/FibProof.thy b/C11-BackEnds/AutoCorres_wrapper/examples/FibProof.thy
index 7d3546b9bae02af406853d950920d312b18f1ea9..c26329e66159a375225f923f93257a4c993b4d2c 100644
--- a/C11-BackEnds/AutoCorres_wrapper/examples/FibProof.thy
+++ b/C11-BackEnds/AutoCorres_wrapper/examples/FibProof.thy
@@ -1,6 +1,7 @@
 (******************************************************************************
  * Isabelle/C/AutoCorres
  *
+ * Copyright (c) 2014, NICTA
  * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France
  *
  * All rights reserved.
diff --git a/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_linear_CCT.thy b/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_linear_CCT.thy
index 081741fb3f91bbeb7981a76a8a14becb3bd934db..09febce1b7b44f6c432988bef885ec3ed05700b0 100644
--- a/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_linear_CCT.thy
+++ b/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_linear_CCT.thy
@@ -1,6 +1,7 @@
 (******************************************************************************
  * Isabelle/C/AutoCorres
  *
+ * Copyright 2014, NICTA (for the C example)
  * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France
  *
  * All rights reserved.
diff --git a/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_CAS.thy b/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_CAS.thy
index 9555f25ea577467e9c7b89beddc3a840238fc3d9..806e7dbdbb1d6f73ec860b898317e20ef4d28819 100644
--- a/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_CAS.thy
+++ b/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_CAS.thy
@@ -1,6 +1,7 @@
 (******************************************************************************
  * Isabelle/C/AutoCorres
  *
+ * Copyright 2014, NICTA (for the C example)
  * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France
  *
  * All rights reserved.
diff --git a/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_TCC.thy b/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_TCC.thy
index d8b5d247dcda0ad12a924ec7efbe3db1c1c88ef7..6e5e1c6b7e8f7dd742222dc76f97e4e5acd2211c 100644
--- a/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_TCC.thy
+++ b/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_TCC.thy
@@ -1,6 +1,7 @@
 (******************************************************************************
  * Isabelle/C/AutoCorres
  *
+ * Copyright (c) 2014, NICTA (for the C example)
  * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France
  *
  * All rights reserved.
diff --git a/C11-BackEnds/AutoCorres_wrapper/examples/ListRev.thy b/C11-BackEnds/AutoCorres_wrapper/examples/ListRev.thy
index 3ef2ffed59fc5ea4373bfa4af7569d5fe0a6c0bf..05f7a8fca2b3e1d2e4fef8b7df7c403454f26cd7 100644
--- a/C11-BackEnds/AutoCorres_wrapper/examples/ListRev.thy
+++ b/C11-BackEnds/AutoCorres_wrapper/examples/ListRev.thy
@@ -1,6 +1,7 @@
 (******************************************************************************
  * Isabelle/C/AutoCorres
  *
+ * Copyright (c) 2014, NICTA (for the C example)
  * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France
  *
  * All rights reserved.
diff --git a/C11-BackEnds/AutoCorres_wrapper/examples/Memcpy.thy b/C11-BackEnds/AutoCorres_wrapper/examples/Memcpy.thy
index c8c12495d0b4efaf96b55049f7dbd96670804044..8a2f2d7b173ea5a416c72a7702b5b4442d57c820 100644
--- a/C11-BackEnds/AutoCorres_wrapper/examples/Memcpy.thy
+++ b/C11-BackEnds/AutoCorres_wrapper/examples/Memcpy.thy
@@ -1,6 +1,7 @@
 (******************************************************************************
  * Isabelle/C/AutoCorres
  *
+ * Copyright (c) 2014, NICTA (for the C sources)
  * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France
  *
  * All rights reserved.
diff --git a/C11-BackEnds/AutoCorres_wrapper/examples/Memset.thy b/C11-BackEnds/AutoCorres_wrapper/examples/Memset.thy
index 5656b9fc5ab30e10bd6281f4f2960e58cfbbb414..281cc22e851d62d3de9e0e4438d9c9b9e8f323e0 100644
--- a/C11-BackEnds/AutoCorres_wrapper/examples/Memset.thy
+++ b/C11-BackEnds/AutoCorres_wrapper/examples/Memset.thy
@@ -1,6 +1,7 @@
 (******************************************************************************
  * Isabelle/C/AutoCorres
  *
+ * Copyright (c) 2014, NICTA (for the C example)
  * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France
  *
  * All rights reserved.
diff --git a/C11-BackEnds/AutoCorres_wrapper/examples/MultByAdd.thy b/C11-BackEnds/AutoCorres_wrapper/examples/MultByAdd.thy
index a4f053ba9d15ae18fed9a9a567bb2fce80ef0eee..1ae977c707147fd60edcbbc72b4a3e083fa9ce40 100644
--- a/C11-BackEnds/AutoCorres_wrapper/examples/MultByAdd.thy
+++ b/C11-BackEnds/AutoCorres_wrapper/examples/MultByAdd.thy
@@ -1,6 +1,7 @@
 (******************************************************************************
  * Isabelle/C/AutoCorres
  *
+ * Copyright (c) 2014, NICTA (for the C example)
  * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France
  *
  * All rights reserved.
diff --git a/C11-BackEnds/AutoCorres_wrapper/examples/Parse_for_loop.thy b/C11-BackEnds/AutoCorres_wrapper/examples/Parse_for_loop.thy
index 74ff7dee120aaba2a3114a8f3c74f7a4d1ecc4b4..895aef6dc5a130ac1b859902a962de0b52ebf598 100644
--- a/C11-BackEnds/AutoCorres_wrapper/examples/Parse_for_loop.thy
+++ b/C11-BackEnds/AutoCorres_wrapper/examples/Parse_for_loop.thy
@@ -1,6 +1,7 @@
 (******************************************************************************
- * Isabelle/C
+ * Isabelle/C/AutoCorres
  *
+ * Copyright 2014, NICTA (for the C example)
  * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France
  *
  * All rights reserved.
diff --git a/C11-BackEnds/AutoCorres_wrapper/examples/Plus.thy b/C11-BackEnds/AutoCorres_wrapper/examples/Plus.thy
index afa163c5a6776c5085ba322c31c64bb6a08a3640..2cada3ae30880b27568bca4bb5b65b2944082806 100644
--- a/C11-BackEnds/AutoCorres_wrapper/examples/Plus.thy
+++ b/C11-BackEnds/AutoCorres_wrapper/examples/Plus.thy
@@ -1,6 +1,7 @@
 (******************************************************************************
  * Isabelle/C/AutoCorres
  *
+ * Copyright (c) 2014, NICTA (for the C example)
  * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France
  *
  * All rights reserved.
diff --git a/C11-BackEnds/AutoCorres_wrapper/examples/Quicksort.thy b/C11-BackEnds/AutoCorres_wrapper/examples/Quicksort.thy
index 503efa0abf84a8ee6b0beea70a756394a38ac1a7..a37f4a2721d9453622208c69d3d6525cf50a632f 100644
--- a/C11-BackEnds/AutoCorres_wrapper/examples/Quicksort.thy
+++ b/C11-BackEnds/AutoCorres_wrapper/examples/Quicksort.thy
@@ -1,6 +1,7 @@
 (******************************************************************************
  * Isabelle/C
  *
+ * Copyright (c) Copyright 2014, NICTA
  * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France
  *
  * All rights reserved.
diff --git a/C11-BackEnds/AutoCorres_wrapper/examples/SchorrWaite.thy b/C11-BackEnds/AutoCorres_wrapper/examples/SchorrWaite.thy
index 6b8cb2bb1cc1df944addbfe124a413ae1f7d658e..0cbf0ca0e3c79c6dad044ed353250c92879005c0 100644
--- a/C11-BackEnds/AutoCorres_wrapper/examples/SchorrWaite.thy
+++ b/C11-BackEnds/AutoCorres_wrapper/examples/SchorrWaite.thy
@@ -1,7 +1,11 @@
 (******************************************************************************
  * Isabelle/C/AutoCorres
  *
+ * Copyright (C) 2003 Farhad Mehta (TUM)
+ * Copyright (C) 2013--2014 Japheth Lim (NICTA)
+ * Copyright (C) 2013--2014 David Greenaway (NICTA)
  * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France
+ *               (for the inclusion in Isabelle/C/AutoCorres
  *
  * All rights reserved.
  *
diff --git a/C11-BackEnds/AutoCorres_wrapper/examples/Simple.thy b/C11-BackEnds/AutoCorres_wrapper/examples/Simple.thy
index 28770270774c05463f153902c3f0a4c0e7e06d62..e194608bee5a7527190aa64e3500ae685c58e9ff 100644
--- a/C11-BackEnds/AutoCorres_wrapper/examples/Simple.thy
+++ b/C11-BackEnds/AutoCorres_wrapper/examples/Simple.thy
@@ -1,6 +1,7 @@
 (******************************************************************************
  * Isabelle/C/AutoCorres
  *
+ * Copyright (c) 2014, NICTA (for the C example)
  * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France
  *
  * All rights reserved.