src/HOL/Nominal/Examples/CR.thy

--- a/src/HOL/Nominal/Examples/CR.thy	Mon Nov 28 00:25:43 2005 +0100
+++ b/src/HOL/Nominal/Examples/CR.thy	Mon Nov 28 05:03:00 2005 +0100
@@ -1,8 +1,11 @@
+(* $Id$ *)
 
 theory cr
 imports lam_substs
 begin
 
+text {* The Church-Rosser proof from Barendregt's book *}
+
 lemma forget[rule_format]: 
   shows "a\<sharp>t1 \<longrightarrow> t1[a::=t2] = t1"
 proof (nominal_induct t1 rule: lam_induct)