# HG changeset patch # User urbanc # Date 1214827604 -7200 # Node ID 1fb3d1219c12fc43d38664327a313b8784acce21 # Parent 768da1da59d67299b27171af359cd6dd410a104f added facts to lemma swap_simps and tuned lemma calc_atms diff -r 768da1da59d6 -r 1fb3d1219c12 src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Mon Jun 30 13:41:33 2008 +0200 +++ b/src/HOL/Nominal/nominal_atoms.ML Mon Jun 30 14:06:44 2008 +0200 @@ -837,7 +837,10 @@ ||>> PureThy.add_thmss [(("alpha_fresh", inst_pt_at [abs_fun_fresh]),[])] ||>> PureThy.add_thmss [(("alpha_fresh'", inst_pt_at [abs_fun_fresh']),[])] ||>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij] @ inst_pt_at [pt_swap_bij']),[])] - ||>> PureThy.add_thmss [(("swap_simps", inst_at at_swap_simps),[])] + ||>> PureThy.add_thmss + let val thms1 = inst_at at_swap_simps + and thms2 = inst_dj [dj_perm_forget] + in [(("swap_simps", thms1 @ thms2),[])] end ||>> PureThy.add_thmss let val thms1 = inst_pt_at [pt_pi_rev]; val thms2 = inst_pt_at [pt_rev_pi]; @@ -866,10 +869,9 @@ val thms2 = inst_dj [at_fresh_ineq] in [(("fresh_atm", thms1 @ thms2),[])] end ||>> PureThy.add_thmss - let val thms1 = filter - (fn th => case prop_of th of _ $ _ $ Var _ => true | _ => false) - (List.concat (List.concat perm_defs)) - in [(("calc_atm", (inst_at at_calc) @ thms1),[])] end + let val thms1 = inst_at at_calc + and thms2 = inst_dj [dj_perm_forget] + in [(("calc_atm", thms1 @ thms2),[])] end ||>> PureThy.add_thmss let val thms1 = inst_pt_at [abs_fun_pi] and thms2 = inst_pt_pt_at_cp [abs_fun_pi_ineq]