diff -r 367f67311e6f -r 7b0c6d07a24e Nominal/Test.thy --- a/Nominal/Test.thy Sun Mar 07 21:30:12 2010 +0100 +++ b/Nominal/Test.thy Sun Mar 07 21:30:57 2010 +0100 @@ -148,7 +148,8 @@ thm lam_bp_perm thm lam_bp_fv thm lam_bp_bn -thm lam_bp_inject*) +thm lam_bp_inject +thm lam_bp_distinct*) text {* example 2 *}