diff --git a/Extended_Finite_State_Machine_Inference/Code_Generation.thy b/Extended_Finite_State_Machine_Inference/Code_Generation.thy
index 6c0609d..d690624 100644
--- a/Extended_Finite_State_Machine_Inference/Code_Generation.thy
+++ b/Extended_Finite_State_Machine_Inference/Code_Generation.thy
@@ -68,12 +68,10 @@ lemma mutex_not_gval:
       apply simp
      apply simp
     apply simp
-    apply (case_tac "s v")
-     apply (case_tac "s v'")
-      apply simp
+    apply (case_tac "s v'")
+     apply simp
     apply simp
-   apply simp
-    apply (case_tac "s v")
+   apply (case_tac "s v")
      apply (case_tac "s v'")
   by auto
 
diff --git a/Extended_Finite_State_Machine_Inference/document/root.bib b/Extended_Finite_State_Machine_Inference/document/root.bib
old mode 100755
new mode 100644
diff --git a/Extended_Finite_State_Machine_Inference/document/root.tex b/Extended_Finite_State_Machine_Inference/document/root.tex
old mode 100755
new mode 100644
index 195a5e6..1f33624
--- a/Extended_Finite_State_Machine_Inference/document/root.tex
+++ b/Extended_Finite_State_Machine_Inference/document/root.tex
@@ -1,5 +1,5 @@
 \documentclass[10pt,DIV16,a4paper,abstract=true,twoside=semi,openright]{scrreprt}
-\usepackage[USenglish]{babel}
+\usepackage[english]{babel}
 \usepackage[numbers, sort&compress]{natbib}
 \usepackage{isabelle,isabellesym}
 \usepackage{booktabs}
@@ -22,8 +22,6 @@
   \begingroup%
   \def\isacharunderscore{\textunderscore}%
   \section{#1 (\thy)}%
-  \def\isacharunderscore{-}%
-  \expandafter\label{sec:\isabellecontext}%
   \endgroup%
 }
 
diff --git a/Extended_Finite_State_Machine_Inference/examples/Drinks_Subsumption.thy b/Extended_Finite_State_Machine_Inference/examples/Drinks_Subsumption.thy
index faba024..7ab4ba9 100644
--- a/Extended_Finite_State_Machine_Inference/examples/Drinks_Subsumption.thy
+++ b/Extended_Finite_State_Machine_Inference/examples/Drinks_Subsumption.thy
@@ -1,5 +1,5 @@
-subsection{*Example*}
-text{*This theory shows how contexts can be used to prove transition subsumption.*}
+subsection\<open>Example\<close> 
+text\<open>This theory shows how contexts can be used to prove transition subsumption.\<close>
 theory Drinks_Subsumption
 imports "Extended_Finite_State_Machine_Inference.Subsumption" "Extended_Finite_State_Machines.Drinks_Machine_2"
 begin
@@ -74,7 +74,6 @@ next
     apply clarify
     apply (simp add: in_possible_steps[symmetric])
     apply (simp add: drinks2_def)
-    apply clarsimp
     apply (simp add: drinks2_def[symmetric])
     apply (simp add: select_def can_take apply_updates_def)
     using no_change_1_1 by fastforce
diff --git a/Extended_Finite_State_Machine_Inference/heuristics/Least_Upper_Bound.thy b/Extended_Finite_State_Machine_Inference/heuristics/Least_Upper_Bound.thy
index 8b8f1f5..e194f7c 100644
--- a/Extended_Finite_State_Machine_Inference/heuristics/Least_Upper_Bound.thy
+++ b/Extended_Finite_State_Machine_Inference/heuristics/Least_Upper_Bound.thy
@@ -704,7 +704,7 @@ next
     apply (induct a)
         apply simp
        apply simp
-    subgoal for _ x2 i ia
+    subgoal for x2 i ia
       apply (case_tac x2)
           apply (rule_tac x="list_update i ia x1" in exI)
           apply (simp add: apply_guards_cons unconstrained_input filter_empty_conv)