# HG changeset patch # User Cezary Kaliszyk # Date 1267516115 -3600 # Node ID 0ab16694c3c1a3e3f6d201a5378b43e9c105f106 # Parent 0ecc775e5fce7084e347d320cb812c1dc7f2fdc9 Add a check of fv_functions. diff -r 0ecc775e5fce -r 0ab16694c3c1 Nominal/Test.thy --- a/Nominal/Test.thy Tue Mar 02 08:42:10 2010 +0100 +++ b/Nominal/Test.thy Tue Mar 02 08:48:35 2010 +0100 @@ -23,6 +23,7 @@ thm bi_raw.simps thm permute_lam_raw_permute_bp_raw.simps thm alpha_lam_raw_alpha_bp_raw.intros +thm fv_lam_raw_fv_bp_raw.simps print_theorems