changeset 19496 | 79dbe35c6cba |
parent 19171 | 17b952ec5641 |
--- a/src/HOL/Nominal/Examples/Lam_substs.thy Fri Apr 28 15:55:38 2006 +0200 +++ b/src/HOL/Nominal/Examples/Lam_substs.thy Fri Apr 28 15:58:30 2006 +0200 @@ -1,10 +1,9 @@ (* $Id$ *) -theory lam_substs -imports "Iteration" +theory Lam_substs +imports Iteration begin - constdefs depth_Var :: "name \<Rightarrow> nat" "depth_Var \<equiv> \<lambda>(a::name). 1"