diff --git a/C11-BackEnds/Clean_wrapper/examples/Coder_Documentation.thy b/C11-BackEnds/Clean_wrapper/examples/Coder_Documentation.thy
index dbbc2b58cbfe5c790753feaa9707509fd1be8162..b31c9c5564ec864c2d7fbe568da518f4487c3cdb 100644
--- a/C11-BackEnds/Clean_wrapper/examples/Coder_Documentation.thy
+++ b/C11-BackEnds/Clean_wrapper/examples/Coder_Documentation.thy
@@ -27,12 +27,12 @@ To prevent Isabelle from coercing types of returned terms \<open>Syntax.parse_te
 Furthermore as parameters are represented as free variables, all constants that would be "selected" through
 a parameter name need to be hidden (\<open>remove_params_from_proof\<close>).
 
-Environment:
+\<^bold>\<open>Environment\<close>:
 The scope of a parameter now is visible in the environment's var table. It is either "Global", "Local" or "Parameter".
 Furthermore each identifier has a field \<open>functionArgs\<close> which is an optional list of function parameters.
 When an identifier has \<open>functionArgs = NONE\<close>, then it is a variable. \<open>functionArgs=SOME []\<close> corresponds to a parameterless function.
 
-Nice to know:
+\<^bold>\<open>Nice to know:\<close>
 - The environment of the last completely parsed C-context can be retrieved using \<open>C_Module.Data_In_Env\<close>.
 - Intermediate envs, containing parameters and local vars can be retrieved using \<open>C_Env.Data_Lang.get'\<close>.
 See C5.thy in the examples of C11-Frontend.
@@ -40,18 +40,17 @@ See C5.thy in the examples of C11-Frontend.
 
 section\<open>Limitations\<close>
 text\<open>
-- Only two types are currently mapped to isabelle types, 
-  namely int -> int and unsigned -> nat.
+\<^item> Only two types are currently mapped to isabelle types, 
+  namely \<^verbatim>\<open>int -> int\<close> and \<^verbatim>\<open>unsigned -> int\<close>.
 
-- Function calls can only occur as statements or on the right hand side of an assignment.
+\<^item> Function calls can only occur as statements or on the right hand side of an assignment.
   For example \<open>a = b + foo();\<close> is not allowed. This must be rewritten as \<open>tmp = foo(); a=b+tmp;\<close>
 
-- Recursive functions must have "void" as return value. This is caused by an issue within
   Clean and is about to be fixed. The current translation should work for this case then.
 
-- Scoping: refrain from defining variables more than once. A read/write from a local variable
+\<^item> Scoping: refrain from defining variables more than once. A read/write from a local variable
   always affects the most recent definition. Scoping using curly braces does not work as in C!
-    example:  
+    Example:  
     \<open>int foo(){
         int x = 3;
         {
@@ -62,12 +61,13 @@ text\<open>
   Also defining global variables twice within one translation unit will result in only one definition, 
   thus the second definition does not "reset" the value of the variable
 
-- Method overloading: Do not use function names multiple times, as this will break the whole
+\<^item> Method overloading: Do not use function names multiple times, as this will break the whole
   translation process in several ways.
 \<close>
 
 section\<open>Some examples\<close>
-text\<open>See \<open>Coder_Test_T_Units\<close> for more examples\<close>
+
+text\<open>See \<open>Coder_Test_T_Units\<close> for more examples:\<close>
 
 C\<open>
 int sum_of_array(int arr[], int length){
@@ -121,7 +121,7 @@ find_theorems multiply
 find_theorems multiply_pre
 find_theorems multiply_post
 
-text\<open>A recursive function calculating the factorial of n\<close>
+text\<open>A recursive function calculating the factorial of \<open>n\<close>\<close>
 C\<open>
 int factorial_result;
 void factorial(int n){
@@ -133,3 +133,5 @@ void factorial(int n){
   }
 }\<close>
 find_theorems factorial_core
+
+end
diff --git a/C11-BackEnds/Clean_wrapper/examples/Coder_Test_Env_AEnv.thy b/C11-BackEnds/Clean_wrapper/examples/Coder_Test_Env_AEnv.thy
index afd008dea198868cf820f09f7f2b8e452e461b1c..e9efd0875f685b018724748e2076abad4a6afa95 100644
--- a/C11-BackEnds/Clean_wrapper/examples/Coder_Test_Env_AEnv.thy
+++ b/C11-BackEnds/Clean_wrapper/examples/Coder_Test_Env_AEnv.thy
@@ -1,10 +1,12 @@
+section \<open>Accessing the \<open>C-Environment\<close> and Conversions to the \<open>Clean Environment\<close>\<close>
+
 theory "Coder_Test_Env_AEnv"
   imports "../src/CleanCoder"
 begin
 
 
 
-section \<open>Accessors to C-Env\<close>
+subsection \<open>Accessors to \<open>C_Env\<close>\<close>
 
 ML\<open>
 fun map_option f (SOME X) = SOME(f X)
@@ -27,8 +29,9 @@ C11_Ast_Lib.toString_nodeinfo;
 C_Ast.SS_base
 \<close>
 
-section \<open>Global Variables, Local Variables, and Local Parameters\<close>
-subsection\<open>An Environment Spy\<close>
+subsection \<open>Global Variables, Local Variables, and Local Parameters\<close>
+
+subsubsection\<open>An Environment Spy\<close>
 
 ML\<open>
 val ENV = Unsynchronized.ref (@{C\<^sub>e\<^sub>n\<^sub>v})
@@ -38,7 +41,6 @@ fun print_env' s _ stack _ env thy =
   in thy end
 \<close>
 
-ML\<open>open Position\<close>
 setup \<open>ML_Antiquotation.inline @{binding print_env'}
                                (Scan.peek (fn _ => Scan.option Parse.embedded)
                                 >> (fn name => ("print_env' "
@@ -46,7 +48,7 @@ setup \<open>ML_Antiquotation.inline @{binding print_env'}
                                                               | SOME s => "(SOME \"" ^ s ^ "\")")
                                                 ^ " " ^ ML_Pretty.make_string_fn)))\<close>
 
-subsection\<open>Accessing the C_Env in an Example\<close>
+subsection\<open>Accessing the \<open>C_Env\<close> in an Example\<close>
 
 C \<comment> \<open>Nesting ML code in C comments\<close> \<open>
 int a(int b){int c; 
@@ -64,8 +66,6 @@ val b_res = lookup_Cid_info (!ENV) "b";
 val c_res = lookup_Cid_info (!ENV) "c"
 \<close>
 
-
-(* Problematic : *)
 C \<comment> \<open>Nesting ML code in C comments\<close> \<open>
 int a (int b){int b; 
               return b;
@@ -80,9 +80,7 @@ lookup_Cid_info (!ENV) "b"
 
 
 
-
-
-section \<open>Global Declarations via CEnv and via the Clean API\<close>
+subsection \<open>Global Declarations via \<open>C_Env\<close> and via the Clean API\<close>
 
 text \<open>
 First, we translate the expressions;
@@ -143,8 +141,6 @@ val [((Some (CDeclr0 (_,t,_,_,_)),_),_)] = B'
 end
 \<close>
 
-ML\<open>(#ret o #3 o the)(lookup_Cid_info env_expr "f" );\<close>
-
 ML\<open>
 C11_TypeSpec_2_CleanTyp.conv_CDerivedDecl_typ;C_Ast.CFunDeclr0;
 val S = hd ((#params o  #3 o the)(lookup_Cid_info env_expr "f" ));
@@ -153,7 +149,6 @@ val S' = C11_TypeSpec_2_CleanTyp.conv_CDerivedDecl_typ [S] sigma_i
 (* and the whole thing a bit more abstract with "a" and "f" *)
 ML\<open>
 map_option (C11_TypeSpec_2_CleanTyp.conv_GlobalIdDescr_typ o #3) (lookup_Cid_info env_expr "a" );
-(* map_option (conv_GlobalIdDescr_typ o #3) (lookup_Cid_info env_expr "f" ); *)
 map_option (C11_TypeSpec_2_CleanTyp.conv_GlobalIdDescr_typ o #3) (lookup_Cid_info env_expr "x" );
 map_option (C11_TypeSpec_2_CleanTyp.conv_GlobalIdDescr_typ o #3) (lookup_Cid_info env_expr "y" );
 \<close>
diff --git a/C11-BackEnds/Clean_wrapper/src/Clean_Wrapper.thy b/C11-BackEnds/Clean_wrapper/src/Clean_Wrapper.thy
index 5d7c7d02062e4394ea7be15c823e16daf927f540..e10d7daff84d600dd5965e662a2c1e8de454fe07 100644
--- a/C11-BackEnds/Clean_wrapper/src/Clean_Wrapper.thy
+++ b/C11-BackEnds/Clean_wrapper/src/Clean_Wrapper.thy
@@ -1,7 +1,7 @@
 (******************************************************************************
  * Isabelle/C/Clean
  *
- * Authors: Frederic Tuong, Burkhart Wolff
+ * Authors: Frederic Tuong, Lorenz Winkler, Burkhart Wolff
  *
  * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France
  *
diff --git a/C11-FrontEnd/main/C_Main.thy b/C11-FrontEnd/main/C_Main.thy
index 35899cbe078c1318a056fb968cbecb4baf1f8257..c82132bf5fbc216eb4d0302f910fbac300a902b5 100644
--- a/C11-FrontEnd/main/C_Main.thy
+++ b/C11-FrontEnd/main/C_Main.thy
@@ -40,5 +40,7 @@ theory C_Main
 begin
 text\<open> @{footnote \<open>sdf\<close>}, @{file "$ISABELLE_HOME/src/Pure/ROOT.ML"}\<close>
 
+
+
 end
 (*>*)