diff --git a/Extended_Finite_State_Machine_Inference/examples/Drinks_Subsumption.thy b/Extended_Finite_State_Machine_Inference/examples/Drinks_Subsumption.thy index 7ab4ba9..96bc310 100644 --- a/Extended_Finite_State_Machine_Inference/examples/Drinks_Subsumption.thy +++ b/Extended_Finite_State_Machine_Inference/examples/Drinks_Subsumption.thy @@ -1,7 +1,7 @@ subsection\Example\ text\This theory shows how contexts can be used to prove transition subsumption.\ theory Drinks_Subsumption -imports "Extended_Finite_State_Machine_Inference.Subsumption" "Extended_Finite_State_Machines.Drinks_Machine_2" +imports "Extended_Finite_State_Machine_Inference-devel.Subsumption" "Extended_Finite_State_Machines.Drinks_Machine_2" begin lemma stop_at_3: "\obtains 1 c drinks2 3 r t"