src/HOL/Nominal/Examples/Iteration.thy

--- a/src/HOL/Nominal/Examples/Iteration.thy	Fri Apr 28 15:55:38 2006 +0200
+++ b/src/HOL/Nominal/Examples/Iteration.thy	Fri Apr 28 15:58:30 2006 +0200
@@ -1,6 +1,7 @@
 (* $Id$ *)
+
 theory Iteration
-imports "../nominal"
+imports "../Nominal"
 begin
 
 atom_decl name
@@ -411,4 +412,5 @@
   also have "\<dots> = f3 b (itfun f1 f2 f3 t)" by (simp add: pt_swap_bij'[OF pt_name_inst, OF at_name_inst])
   finally show ?thesis by simp
 qed
+
 end