diff --git a/Extended_Finite_State_Machines/EFSM_LTL.thy b/Extended_Finite_State_Machines/EFSM_LTL.thy
index 00951b5..de8c509 100644
--- a/Extended_Finite_State_Machines/EFSM_LTL.thy
+++ b/Extended_Finite_State_Machines/EFSM_LTL.thy
@@ -4,7 +4,7 @@ library and defines functions to ease the expression of LTL properties over EFSM
 operators effectively act over traces of models we must find a way to express models as streams.\<close>
 
 theory EFSM_LTL
-imports "Extended_Finite_State_Machines.EFSM" "HOL-Library.Linear_Temporal_Logic_on_Streams"
+imports "Extended_Finite_State_Machines-devel.EFSM" "HOL-Library.Linear_Temporal_Logic_on_Streams"
 begin
 
 text_raw\<open>\snip{statedef}{1}{2}{%\<close>
diff --git a/Extended_Finite_State_Machines/examples/Drinks_Machine.thy b/Extended_Finite_State_Machines/examples/Drinks_Machine.thy
index af7466b..c3047a7 100644
--- a/Extended_Finite_State_Machines/examples/Drinks_Machine.thy
+++ b/Extended_Finite_State_Machines/examples/Drinks_Machine.thy
@@ -15,7 +15,7 @@ Note that, while statename has four elements, the drinks machine presented here
 states. The fourth element is included here so that the \emph{statename} datatype may be used in
 the next example.\<close>
 theory Drinks_Machine
-  imports "Extended_Finite_State_Machines.EFSM"
+  imports "Extended_Finite_State_Machines-devel.EFSM"
 begin
 
 text_raw\<open>\snip{selectdef}{1}{2}{%\<close>
diff --git a/Extended_Finite_State_Machines/examples/Drinks_Machine_LTL.thy b/Extended_Finite_State_Machines/examples/Drinks_Machine_LTL.thy
index 620c785..09b3ead 100644
--- a/Extended_Finite_State_Machines/examples/Drinks_Machine_LTL.thy
+++ b/Extended_Finite_State_Machines/examples/Drinks_Machine_LTL.thy
@@ -2,7 +2,7 @@ section\<open>Temporal Properties\<close>
 text\<open>This theory presents some examples of temporal properties over the simple drinks machine.\<close>
 
 theory Drinks_Machine_LTL
-imports "Drinks_Machine" "Extended_Finite_State_Machines.EFSM_LTL"
+imports "Drinks_Machine" "Extended_Finite_State_Machines-devel.EFSM_LTL"
 begin
 
 declare One_nat_def [simp del]