# HG changeset patch # User urbanc # Date 1152021439 -7200 # Node ID bb383dcec3d8f134f2f113c3258de45aad8c685d # Parent 0c9650664d47f64479aa499b192a31078fe6a6b0 made calc_atm stronger by including some relative obvious simplification rules diff -r 0c9650664d47 -r bb383dcec3d8 src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Tue Jul 04 15:45:59 2006 +0200 +++ b/src/HOL/Nominal/nominal_atoms.ML Tue Jul 04 15:57:19 2006 +0200 @@ -771,7 +771,11 @@ let val thms1 = inst_at [at_fresh] val thms2 = inst_dj [at_fresh_ineq] in [(("fresh_atm", thms1 @ thms2),[])] end - ||>> PureThy.add_thmss [(("calc_atm", inst_at at_calc),[])] + ||>> PureThy.add_thmss + let val thms1 = List.concat (List.concat perm_defs) + val thms2 = List.concat prm_eqs + val thms3 = List.concat swap_eqs + in [(("calc_atm", (inst_at at_calc) @ thms1 @ thms2 @ thms3 ),[])] end ||>> PureThy.add_thmss let val thms1 = inst_pt_at [abs_fun_pi] and thms2 = inst_pt_pt_at_cp [abs_fun_pi_ineq]