--- a/src/HOL/UNITY/Simple/Deadlock.thy Sat Sep 10 21:47:55 2011 +0200
+++ b/src/HOL/UNITY/Simple/Deadlock.thy Sat Sep 10 22:11:55 2011 +0200
@@ -6,11 +6,11 @@
Misra, "A Logic for Concurrent Programming", 1994
*)
-theory Deadlock imports UNITY begin
+theory Deadlock imports "../UNITY" begin
(*Trivial, two-process case*)
lemma "[| F \<in> (A \<inter> B) co A; F \<in> (B \<inter> A) co B |] ==> F \<in> stable (A \<inter> B)"
-by (unfold constrains_def stable_def, blast)
+ unfolding constrains_def stable_def by blast
(*a simplification step*)