src/HOL/Nominal/Examples/Lam_substs.thy
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"