Capitalized theory names.

--- a/src/HOL/Nominal/Examples/CR.thy	Fri Apr 28 15:55:38 2006 +0200
+++ b/src/HOL/Nominal/Examples/CR.thy	Fri Apr 28 15:58:30 2006 +0200
@@ -1,7 +1,7 @@
 (* $Id$ *)
 
 theory CR
-imports lam_substs
+imports Lam_substs
 begin
 
 text {* The Church-Rosser proof from Barendregt's book *}

--- 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

--- 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"

--- a/src/HOL/Nominal/Examples/SN.thy	Fri Apr 28 15:55:38 2006 +0200
+++ b/src/HOL/Nominal/Examples/SN.thy	Fri Apr 28 15:58:30 2006 +0200
@@ -1,7 +1,7 @@
 (* $Id$ *)
 
-theory sn
-imports lam_substs  Accessible_Part
+theory SN
+imports Lam_substs Accessible_Part
 begin
 
 text {* Strong Normalisation proof from the Proofs and Types book *}

--- a/src/HOL/Nominal/Examples/Weakening.thy	Fri Apr 28 15:55:38 2006 +0200
+++ b/src/HOL/Nominal/Examples/Weakening.thy	Fri Apr 28 15:58:30 2006 +0200
@@ -1,7 +1,7 @@
 (* $Id$ *)
 
-theory weakening 
-imports "../nominal" 
+theory Weakening 
+imports "../Nominal" 
 begin
 
 (* WEAKENING EXAMPLE*)
@@ -230,6 +230,6 @@
   have "((a,\<tau>)#\<Gamma>1) \<lless> ((a,\<tau>)#\<Gamma>2)" using a2 by (simp add: sub_def)
   moreover
   have "valid ((a,\<tau>)#\<Gamma>2)" using v2 (* fails *) 
-
+    oops
 
-
+end
\ No newline at end of file