Nominal/Ex/SFT/Lambda.thy
changeset 2898 a95a497e1f4f
parent 2894 8ec94871de1e
child 2984 1b39ba5db2c1
--- a/Nominal/Ex/SFT/Lambda.thy	Fri Jun 24 11:15:22 2011 +0900
+++ b/Nominal/Ex/SFT/Lambda.thy	Fri Jun 24 11:18:18 2011 +0900
@@ -1,6 +1,6 @@
 header {* Definition of Lambda terms and convertibility *}
 
-theory Lambda imports Nominal2 begin
+theory Lambda imports "../../Nominal2" begin
 
 lemma [simp]: "supp x = {} \<Longrightarrow> y \<sharp> x"
   unfolding fresh_def by blast