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