# HG changeset patch
# User berghofe
# Date 1146232710 -7200
# Node ID 79dbe35c6cbaeb042eb16b26c7748b29c889e650
# Parent  3d04b87ad8ba4c1f6415c72f1acb717ecbfe992d
Capitalized theory names.

diff -r 3d04b87ad8ba -r 79dbe35c6cba src/HOL/Nominal/Examples/CR.thy
--- 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 *}
diff -r 3d04b87ad8ba -r 79dbe35c6cba 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
diff -r 3d04b87ad8ba -r 79dbe35c6cba src/HOL/Nominal/Examples/Lam_substs.thy
--- 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"
diff -r 3d04b87ad8ba -r 79dbe35c6cba src/HOL/Nominal/Examples/SN.thy
--- 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 *}
diff -r 3d04b87ad8ba -r 79dbe35c6cba src/HOL/Nominal/Examples/Weakening.thy
--- 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