made calc_atm stronger by including some relative
authorurbanc
Tue Jul 04 15:57:19 2006 +0200 (2006-07-04)
changeset 19992bb383dcec3d8
parent 19991 0c9650664d47
child 19993 e0a5783d708f
made calc_atm stronger by including some relative
obvious simplification rules
src/HOL/Nominal/nominal_atoms.ML
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Tue Jul 04 15:45:59 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Jul 04 15:57:19 2006 +0200
     1.3 @@ -771,7 +771,11 @@
     1.4  	      let val thms1 = inst_at [at_fresh]
     1.5  		  val thms2 = inst_dj [at_fresh_ineq]
     1.6  	      in [(("fresh_atm", thms1 @ thms2),[])] end
     1.7 -            ||>> PureThy.add_thmss [(("calc_atm", inst_at at_calc),[])]
     1.8 +            ||>> PureThy.add_thmss
     1.9 +	      let val thms1 = List.concat (List.concat perm_defs)
    1.10 +                  val thms2 = List.concat prm_eqs
    1.11 +                  val thms3 = List.concat swap_eqs
    1.12 +              in [(("calc_atm", (inst_at at_calc) @ thms1 @ thms2 @ thms3 ),[])] end
    1.13              ||>> PureThy.add_thmss
    1.14  	      let val thms1 = inst_pt_at [abs_fun_pi]
    1.15  		  and thms2 = inst_pt_pt_at_cp [abs_fun_pi_ineq]