src/HOL/Nominal/Examples/CR.thy
changeset 21138 afdd72fc6c4f
parent 21101 286d68ce3f5b
child 21143 56695d1f45cf
--- a/src/HOL/Nominal/Examples/CR.thy	Wed Nov 01 15:51:11 2006 +0100
+++ b/src/HOL/Nominal/Examples/CR.thy	Wed Nov 01 16:11:31 2006 +0100
@@ -1,7 +1,7 @@
 (* $Id$ *)
 
 theory CR
-imports Lam_substs
+imports Lam_Funs
 begin
 
 text {* The Church-Rosser proof from Barendregt's book *}